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		mercolem3	$⊢ (ψ \to χ) \to (ψ \to (φ \to χ))$
2		mercolem8	$⊢ (φ \to ψ) \to ((ψ \to (φ \to χ)) \to ((φ \to ψ) \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	2 3	ax-mp	$⊢ (ψ \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
5		mercolem3	$⊢ ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to ((ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))$
6	4 5	ax-mp	$⊢ (ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
7		mercolem8	$⊢ ((ψ \to χ) \to (ψ \to (φ \to χ))) \to (((ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (ψ \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))))$
8		mercolem6	$⊢ (((ψ \to χ) \to (ψ \to (φ \to χ))) \to (((ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (ψ \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))))) \to (((ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (ψ \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))))$
9	7 8	ax-mp	$⊢ ((ψ \to (φ \to χ)) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (ψ \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))))$
10	6 9	ax-mp	$⊢ ((ψ \to χ) \to (ψ \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))$
11	1 10	ax-mp	$⊢ (φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
12		mercolem6	$⊢ ((φ \to ψ) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
13	11 12	ax-mp	$⊢ (ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
14		mercolem6	$⊢ ((ψ \to χ) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
15	13 14	ax-mp	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$