Metamath Proof Explorer

Theorem re1ax2lem

Description: Lemma for re1ax2 . (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion re1ax2lem ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 tb-ax2 ⊢ ( 𝜓 → ( ( 𝜓 → 𝜒 ) → 𝜓 ) )
2 tb-ax1 ⊢ ( ( ( 𝜓 → 𝜒 ) → 𝜓 ) → ( ( 𝜓 → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) )
3 1 2 tbsyl ⊢ ( 𝜓 → ( ( 𝜓 → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) )
4 tb-ax1 ⊢ ( ( ( 𝜓 → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) → ( ( ( ( 𝜓 → 𝜒 ) → 𝜒 ) → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) )
5 tb-ax3 ⊢ ( ( ( ( ( 𝜓 → 𝜒 ) → 𝜒 ) → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) )
6 4 5 tbsyl ⊢ ( ( ( 𝜓 → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) → ( ( 𝜓 → 𝜒 ) → 𝜒 ) )
7 3 6 tbsyl ⊢ ( 𝜓 → ( ( 𝜓 → 𝜒 ) → 𝜒 ) )
8 tb-ax1 ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( 𝜓 → 𝜒 ) → 𝜒 ) → ( 𝜑 → 𝜒 ) ) )
9 tb-ax1 ⊢ ( ( 𝜓 → ( ( 𝜓 → 𝜒 ) → 𝜒 ) ) → ( ( ( ( 𝜓 → 𝜒 ) → 𝜒 ) → ( 𝜑 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) ) )
10 7 8 9 mpsyl ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) )