Metamath Proof Explorer


Theorem luk-2

Description: 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion luk-2 ¬ φ φ φ

Proof

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