Theorem merlem11 1417

Description: Step 20 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
merlem11	⊢ ((φ → (φ → ψ)) → (φ → ψ))

Proof of Theorem merlem11

Step	Hyp	Ref	Expression
1		ax-meredith 1406	. 2 ⊢ (((((φ → φ) → (¬ φ → ¬ φ)) → φ) → φ) → ((φ → φ) → (φ → φ)))
2		merlem10 1416	. . 3 ⊢ ((φ → (φ → ψ)) → ((φ → (φ → ψ)) → (φ → ψ)))
3		merlem10 1416	. . 3 ⊢ (((φ → (φ → ψ)) → ((φ → (φ → ψ)) → (φ → ψ))) → ((((((φ → φ) → (¬ φ → ¬ φ)) → φ) → φ) → ((φ → φ) → (φ → φ))) → ((φ → (φ → ψ)) → (φ → ψ))))
4	2, 3	ax-mp 5	. 2 ⊢ ((((((φ → φ) → (¬ φ → ¬ φ)) → φ) → φ) → ((φ → φ) → (φ → φ))) → ((φ → (φ → ψ)) → (φ → ψ)))
5	1, 4	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  luk-3  1422