Theorem com45 97

Description: Commutation of antecedents. Swap 4th and 5th. Deduction associated with com34 91. Double deduction associated with com23 86. Triple deduction associated with com12 32. (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 90	. 2 ⊢ ((𝜃 → (𝜏 → 𝜂)) → (𝜏 → (𝜃 → 𝜂)))
3	1, 2	syl8 76	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  98  com25  99  com5l  100  ad5ant13  1301  ad5ant14  1302  ad5ant15  1303  ad5ant23  1304  ad5ant24  1305  ad5ant25  1306  ad5ant235  1309  ad5ant123  1310  ad5ant124  1311  ad5ant134  1313  ad5ant135  1314  lcmfdvdsb  15356  prmgaplem6  15760  islmhm2  19038  dfon2lem8  31695