Metamath Proof Explorer

Theorem frege34

Description: If as a conseqence of the occurrence of the circumstance ph , when the obstacle ps is removed, ch takes place, then from the circumstance that ch does not take place while ph occurs the occurrence of the obstacle ps can be inferred. Closed form of con1d . Proposition 34 of Frege1879 p. 45. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege34 
|- ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) )

Proof

Step Hyp Ref Expression
1 frege33 
 |-  ( ( -. ps -> ch ) -> ( -. ch -> ps ) )
2 frege5 
 |-  ( ( ( -. ps -> ch ) -> ( -. ch -> ps ) ) -> ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) )