Metamath Proof Explorer


Theorem merlem5

Description: Step 11 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 merlem5 φ ψ ¬ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 meredith ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ
2 meredith ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ φ ψ ¬ ¬ φ ψ
3 merlem1 φ ψ ¬ ¬ φ ψ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ ¬ φ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ
4 merlem4 φ ψ ¬ ¬ φ ψ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ ¬ φ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ¬ ¬ φ ψ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ ¬ φ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ
5 3 4 ax-mp φ ψ ¬ ¬ φ ψ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ ¬ φ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ
6 meredith φ ψ ¬ ¬ φ ψ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ ¬ φ ¬ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ φ ψ ¬ ¬ φ ψ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ¬ ¬ φ ψ
7 5 6 ax-mp ψ ψ ¬ ψ ¬ ¬ ¬ φ ψ φ φ ψ ¬ ¬ φ ψ ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ¬ ¬ φ ψ
8 2 7 ax-mp ψ ψ ¬ ψ ¬ ψ ψ ψ ψ ψ ψ ψ φ ψ ¬ ¬ φ ψ
9 1 8 ax-mp φ ψ ¬ ¬ φ ψ