re1ax2

Description: ax-2 rederived from the Tarski-Bernays axiom system. Often tb-ax1 is replaced with this theorem to make a "standard" system. This is because this theorem is easier to work with, despite it being longer. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		re1ax2lem	$⊢ (φ \to (ψ \to χ)) \to (ψ \to (φ \to χ))$
2		tb-ax1	$⊢ (φ \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))$
3		tb-ax3	$⊢ (((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)$
4	2 3	tbsyl	$⊢ (φ \to (φ \to χ)) \to (φ \to χ)$
5		tb-ax1	$⊢ (φ \to ψ) \to ((ψ \to (φ \to χ)) \to (φ \to (φ \to χ)))$
6		re1ax2lem	$⊢ ((φ \to ψ) \to ((ψ \to (φ \to χ)) \to (φ \to (φ \to χ)))) \to ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to (φ \to χ))))$
7	5 6	ax-mp	$⊢ (ψ \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to (φ \to χ)))$
8		tb-ax1	$⊢ ((φ \to ψ) \to (φ \to (φ \to χ))) \to (((φ \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))$
9		re1ax2lem	$⊢ (((φ \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 χ))))$
10	8 9	ax-mp	$⊢ ((φ \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to ψ) \to (φ \to (φ \to χ))) \to ((φ \to ψ) \to (φ \to χ)))$
11	4 7 10	mpsyl	$⊢ (ψ \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$
12	1 11	tbsyl	$⊢ (φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$

Metamath Proof Explorer

Theorem re1ax2

Proof