Theorem merlem5 649

Description: Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

Assertion

Ref	Expression
merlem5	⊢ ((φ → ψ) → (¬ ¬ φ → ψ))

Proof of Theorem merlem5

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

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  merlem12 656  merlem13 657  luk-2 659

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

metamath.org