Theorem luk-2 659

Description: 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.

Assertion

Ref	Expression
luk-2	⊢ ((¬ φ → φ) → φ)

Proof of Theorem luk-2

Step	Hyp	Ref	Expression
1		merlem5 649	. . . . 5 ⊢ ((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ)))
2		merlem4 648	. . . . 5 ⊢ (((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ)))
3	1, 2	ax-mp 6	. . . 4 ⊢ ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ))
4		merlem11 655	. . . 4 ⊢ (((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ)) → ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ))
5	3, 4	ax-mp 6	. . 3 ⊢ ((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ)
6		meredith 644	. . 3 ⊢ (((((φ → ¬ (¬ φ → φ)) → (¬ ¬ φ → ¬ (¬ φ → φ))) → ¬ φ) → ¬ φ) → ((¬ φ → φ) → ((¬ φ → φ) → φ)))
7	5, 6	ax-mp 6	. 2 ⊢ ((¬ φ → φ) → ((¬ φ → φ) → φ))
8		merlem11 655	. 2 ⊢ (((¬ φ → φ) → ((¬ φ → φ) → φ)) → ((¬ φ → φ) → φ))
9	7, 8	ax-mp 6	1 ⊢ ((¬ φ → φ) → φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  luklem4 664

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org