Theorem merlem3 647

Description: Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

Assertion

Ref	Expression
merlem3	⊢ (((ψ → χ) → φ) → (χ → φ))

Proof of Theorem merlem3

Step	Hyp	Ref	Expression
1		merlem2 646	. . . 4 ⊢ (((¬ χ → ¬ χ) → (¬ χ → ¬ χ)) → ((φ → φ) → (¬ χ → ¬ χ)))
2		merlem2 646	. . . 4 ⊢ ((((¬ χ → ¬ χ) → (¬ χ → ¬ χ)) → ((φ → φ) → (¬ χ → ¬ χ))) → ((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ))))
3	1, 2	ax-mp 6	. . 3 ⊢ ((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ)))
4		meredith 644	. . 3 ⊢ (((((χ → φ) → (¬ ψ → ¬ ψ)) → ψ) → ((φ → φ) → (¬ χ → ¬ χ))) → ((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ)))
5	3, 4	ax-mp 6	. 2 ⊢ ((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ))
6		meredith 644	. 2 ⊢ (((((φ → φ) → (¬ χ → ¬ χ)) → χ) → (ψ → χ)) → (((ψ → χ) → φ) → (χ → φ)))
7	5, 6	ax-mp 6	1 ⊢ (((ψ → χ) → φ) → (χ → φ))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  merlem4 648  merlem6 650

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

metamath.org