Metamath Proof Explorer


Theorem frege60a

Description: Swap antecedents of ax-frege58a . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 17-Apr-2020) (Proof modification is discouraged.)

Ref Expression
Assertion frege60a ψχθτηζif-φχηif-φψτif-φθζ

Proof

Step Hyp Ref Expression
1 frege58acor ψχθτηζif-φψτif-φχθηζ
2 ifpimim if-φχθηζif-φχηif-φθζ
3 1 2 syl6 ψχθτηζif-φψτif-φχηif-φθζ
4 frege12 ψχθτηζif-φψτif-φχηif-φθζψχθτηζif-φχηif-φψτif-φθζ
5 3 4 ax-mp ψχθτηζif-φχηif-φψτif-φθζ