Metamath Proof Explorer


Theorem frege49

Description: Closed form of deduction with disjunction. Proposition 49 of Frege1879 p. 49. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege49 ¬ φ ψ φ χ ψ χ χ

Proof

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