Metamath Proof Explorer


Theorem frege57a

Description: Analogue of frege57aid . Proposition 57 of Frege1879 p. 51. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege57a φψif-ψχθif-φχθ

Proof

Step Hyp Ref Expression
1 ax-frege52a ψφif-ψχθif-φχθ
2 frege56a ψφif-ψχθif-φχθφψif-ψχθif-φχθ
3 1 2 ax-mp φψif-ψχθif-φχθ