Metamath Proof Explorer

Theorem frege51

Description: Compare with jaod . Proposition 51 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 frege50 
 |-  ( ( ps -> ch ) -> ( ( th -> ch ) -> ( ( -. ps -> th ) -> ch ) ) )
2 frege18 
 |-  ( ( ( ps -> ch ) -> ( ( th -> ch ) -> ( ( -. ps -> th ) -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ch ) -> ( ph -> ( ( -. ps -> th ) -> ch ) ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ch ) -> ( ph -> ( ( -. ps -> th ) -> ch ) ) ) )