Theorem merlem5 1411

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.)

Assertion

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

Proof of Theorem merlem5

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-meredith 1406

This theorem is used by:  merlem12  1418  merlem13  1419  luk-2  1421