Metamath Proof Explorer


Theorem frege35

Description: Commuted, closed form of con1d . Proposition 35 of Frege1879 p. 45. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege35 φ ¬ ψ χ ¬ χ φ ψ

Proof

Step Hyp Ref Expression
1 frege34 φ ¬ ψ χ φ ¬ χ ψ
2 frege12 φ ¬ ψ χ φ ¬ χ ψ φ ¬ ψ χ ¬ χ φ ψ
3 1 2 ax-mp φ ¬ ψ χ ¬ χ φ ψ