Metamath Proof Explorer

Theorem re1tbw1

Description: tbw-ax1 rederived from merco2 . (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	re1tbw1	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		mercolem8	$⊢ (φ \to ψ) \to ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
2		mercolem3	$⊢ (ψ \to χ) \to (ψ \to (φ \to χ))$
3		mercolem6	$⊢ ((φ \to ψ) \to ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
4	1 2 3	mpsyl	$⊢ (ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
5		mercolem6	$⊢ ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
6	4 5	ax-mp	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$