Theorem merlem5 1654

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		meredith 1649	. 2 ⊢ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))
2		meredith 1649	. . 3 ⊢ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)))
3		merlem1 1650	. . . . 5 ⊢ ((((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))) → (¬ 𝜑 → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))))
4		merlem4 1653	. . . . 5 ⊢ (((((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))) → (¬ 𝜑 → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))))) → ((((((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))) → (¬ 𝜑 → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))))) → 𝜑) → ((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑)))
5	3, 4	ax-mp 5	. . . 4 ⊢ ((((((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))) → (¬ 𝜑 → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))))) → 𝜑) → ((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑))
6		meredith 1649	. . . 4 ⊢ (((((((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓)))) → (¬ 𝜑 → ¬ (((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))))) → 𝜑) → ((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑)) → ((((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓))) → ((((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)))))
7	5, 6	ax-mp 5	. . 3 ⊢ ((((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ ¬ ¬ 𝜑)) → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓))) → ((((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓))))
8	2, 7	ax-mp 5	. 2 ⊢ ((((((𝜓 → 𝜓) → (¬ 𝜓 → ¬ 𝜓)) → 𝜓) → 𝜓) → ((𝜓 → 𝜓) → (𝜓 → 𝜓))) → ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)))
9	1, 8	ax-mp 5	1 ⊢ ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  merlem12  1661  merlem13  1662  luk-2  1664