Metamath Proof Explorer

Theorem frege4

Description: Special case of closed form of a2d . Special case of rp-frege4g . Proposition 4 of Frege1879 p. 31. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege4 
|- ( ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) ) -> ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )

Proof

Step Hyp Ref Expression
1 frege3 
 |-  ( ( ph -> ps ) -> ( ( ch -> ( ph -> ps ) ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )
2 ax-frege2 
 |-  ( ( ( ph -> ps ) -> ( ( ch -> ( ph -> ps ) ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) ) -> ( ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) ) -> ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) ) -> ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )