Metamath Proof Explorer


Theorem frege30

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

Ref Expression
Assertion frege30 φ ψ χ ψ ¬ χ ¬ φ

Proof

Step Hyp Ref Expression
1 frege29 ψ φ χ ψ ¬ χ ¬ φ
2 frege10 ψ φ χ ψ ¬ χ ¬ φ φ ψ χ ψ ¬ χ ¬ φ
3 1 2 ax-mp φ ψ χ ψ ¬ χ ¬ φ