Metamath Proof Explorer


Theorem frege60c

Description: Swap antecedents of frege58c . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege59c.a A B
Assertion frege60c x φ ψ χ [˙A / x]˙ ψ [˙A / x]˙ φ [˙A / x]˙ χ

Proof

Step Hyp Ref Expression
1 frege59c.a A B
2 1 frege58c x φ ψ χ [˙A / x]˙ φ ψ χ
3 sbcim1 [˙A / x]˙ φ ψ χ [˙A / x]˙ φ [˙A / x]˙ ψ χ
4 sbcim1 [˙A / x]˙ ψ χ [˙A / x]˙ ψ [˙A / x]˙ χ
5 3 4 syl6 [˙A / x]˙ φ ψ χ [˙A / x]˙ φ [˙A / x]˙ ψ [˙A / x]˙ χ
6 2 5 syl x φ ψ χ [˙A / x]˙ φ [˙A / x]˙ ψ [˙A / x]˙ χ
7 frege12 x φ ψ χ [˙A / x]˙ φ [˙A / x]˙ ψ [˙A / x]˙ χ x φ ψ χ [˙A / x]˙ ψ [˙A / x]˙ φ [˙A / x]˙ χ
8 6 7 ax-mp x φ ψ χ [˙A / x]˙ ψ [˙A / x]˙ φ [˙A / x]˙ χ