Metamath Proof Explorer

Theorem frege32

Description: Deduce con1 from con3 . Proposition 32 of Frege1879 p. 44. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege32 
|- ( ( ( -. ph -> ps ) -> ( -. ps -> -. -. ph ) ) -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) )

Proof

Step Hyp Ref Expression
1 ax-frege31 
 |-  ( -. -. ph -> ph )
2 frege7 
 |-  ( ( -. -. ph -> ph ) -> ( ( ( -. ph -> ps ) -> ( -. ps -> -. -. ph ) ) -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ( -. ph -> ps ) -> ( -. ps -> -. -. ph ) ) -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) )