Theorem merlem4 1410

Description: Step 8 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
merlem4	⊢ (τ → ((τ → φ) → (θ → φ)))

Proof of Theorem merlem4

Step	Hyp	Ref	Expression
1		ax-meredith 1406	. 2 ⊢ (((((φ → φ) → (¬ θ → ¬ θ)) → θ) → τ) → ((τ → φ) → (θ → φ)))
2		merlem3 1409	. 2 ⊢ ((((((φ → φ) → (¬ θ → ¬ θ)) → θ) → τ) → ((τ → φ) → (θ → φ))) → (τ → ((τ → φ) → (θ → φ))))
3	1, 2	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:  merlem5  1411  merlem6  1412  merlem7  1413  merlem12  1418  luk-2  1421