Metamath Proof Explorer


Theorem merlem3

Description: Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion merlem3 ψ χ φ χ φ

Proof

Step Hyp Ref Expression
1 merlem2 ¬ χ ¬ χ ¬ χ ¬ χ φ φ ¬ χ ¬ χ
2 merlem2 ¬ χ ¬ χ ¬ χ ¬ χ φ φ ¬ χ ¬ χ χ φ ¬ ψ ¬ ψ ψ φ φ ¬ χ ¬ χ
3 1 2 ax-mp χ φ ¬ ψ ¬ ψ ψ φ φ ¬ χ ¬ χ
4 meredith χ φ ¬ ψ ¬ ψ ψ φ φ ¬ χ ¬ χ φ φ ¬ χ ¬ χ χ ψ χ
5 3 4 ax-mp φ φ ¬ χ ¬ χ χ ψ χ
6 meredith φ φ ¬ χ ¬ χ χ ψ χ ψ χ φ χ φ
7 5 6 ax-mp ψ χ φ χ φ