Theorem merlem3 1409

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

Proof of Theorem merlem3

Step	Hyp	Ref	Expression
1		merlem2 1408	. . . 4 ⊢ (((¬ χ → ¬ χ) → (¬ χ → ¬ χ)) → ((φ → φ) → (¬ χ → ¬ χ)))
2		merlem2 1408	. . . 4 ⊢ ((((¬ χ → ¬ χ) → (¬ χ → ¬ χ)) → ((φ → φ) → (¬ χ → ¬ χ))) → ((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ))))
3	1, 2	ax-mp 5	. . 3 ⊢ ((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ)))
4		ax-meredith 1406	. . 3 ⊢ (((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ))) → ((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ)))
5	3, 4	ax-mp 5	. 2 ⊢ ((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ))
6		ax-meredith 1406	. 2 ⊢ (((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ)) → (((ψ → χ) → φ) → (χ → φ)))
7	5, 6	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:  merlem4  1410  merlem6  1412