Theorem merlem5 1679

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

This theorem is used by:  merlem12  1686  merlem13  1687  luk-2  1689