Theorem com45 95

Description: Commutation of antecedents. Swap 4th and 5th. Deduction associated with com34 89. (Contributed by Jeff Hankins, 28-Jun-2009.)

Hypothesis

Ref	Expression
com5.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))

Assertion

Ref	Expression
com45	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂)))))

Proof of Theorem com45

Step	Hyp	Ref	Expression
1		com5.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
2		pm2.04 88	. 2 ⊢ ((𝜃 → (𝜏 → 𝜂)) → (𝜏 → (𝜃 → 𝜂)))
3	1, 2	syl8 74	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂)))))

Syntax hints:   → wi 4

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

This theorem is referenced by:  com35  96  com25  97  com5l  98  ad5ant13  1293  ad5ant14  1294  ad5ant15  1295  ad5ant23  1296  ad5ant24  1297  ad5ant25  1298  ad5ant235  1301  ad5ant123  1302  ad5ant124  1303  ad5ant134  1305  ad5ant135  1306  lcmfdvdsb  15194  prmgaplem6  15598  islmhm2  18859  dfon2lem8  30939