Metamath Proof Explorer

Theorem frege64c

Description: Lemma for frege65c . Proposition 64 of Frege1879 p. 53. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege59c.a 
|- A e. B
Assertion frege64c 
|- ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) )

Proof

Step Hyp Ref Expression
1 frege59c.a 
 |-  A e. B
2 1 frege62c 
 |-  ( [. A / x ]. ps -> ( A. x ( ps -> ch ) -> [. A / x ]. ch ) )
3 frege18 
 |-  ( ( [. A / x ]. ps -> ( A. x ( ps -> ch ) -> [. A / x ]. ch ) ) -> ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) ) )
4 2 3 ax-mp 
 |-  ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) )