Metamath Proof Explorer


Theorem merlem8

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

Ref Expression
Assertion merlem8 ψ χ θ χ τ ¬ θ ¬ ψ θ

Proof

Step Hyp Ref Expression
1 meredith φ φ ¬ φ ¬ φ φ φ φ φ φ φ
2 merlem7 φ φ ¬ φ ¬ φ φ φ φ φ φ φ ψ χ θ χ τ ¬ θ ¬ ψ θ
3 1 2 ax-mp ψ χ θ χ τ ¬ θ ¬ ψ θ