Metamath Proof Explorer


Theorem merlem1

Description: Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion merlem1 χ ¬ φ ψ τ φ τ

Proof

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