Metamath Proof Explorer


Theorem merlem7

Description: Between steps 14 and 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 merlem7 φ ψ χ θ χ τ ¬ θ ¬ ψ θ

Proof

Step Hyp Ref Expression
1 merlem4 ψ χ ψ χ θ χ τ ¬ θ ¬ ψ θ
2 merlem6 χ τ ¬ θ ¬ ψ θ ψ χ θ χ τ ¬ θ ¬ ψ θ ¬ φ ¬ χ ¬ φ
3 meredith χ τ ¬ θ ¬ ψ θ ψ χ θ χ τ ¬ θ ¬ ψ θ ¬ φ ¬ χ ¬ φ ψ χ θ χ τ ¬ θ ¬ ψ θ ¬ φ ¬ χ ¬ φ χ ψ χ
4 2 3 ax-mp ψ χ θ χ τ ¬ θ ¬ ψ θ ¬ φ ¬ χ ¬ φ χ ψ χ
5 meredith ψ χ θ χ τ ¬ θ ¬ ψ θ ¬ φ ¬ χ ¬ φ χ ψ χ ψ χ ψ χ θ χ τ ¬ θ ¬ ψ θ φ ψ χ θ χ τ ¬ θ ¬ ψ θ
6 4 5 ax-mp ψ χ ψ χ θ χ τ ¬ θ ¬ ψ θ φ ψ χ θ χ τ ¬ θ ¬ ψ θ
7 1 6 ax-mp φ ψ χ θ χ τ ¬ θ ¬ ψ θ