MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com45 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com5.1 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
2 pm2.04 90 . 2 ((𝜃 → (𝜏𝜂)) → (𝜏 → (𝜃𝜂)))
31, 2syl8 76 1 (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃𝜂)))))
Colors of variables: wff setvar class
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  1298  ad5ant14  1299  ad5ant15  1300  ad5ant23  1301  ad5ant24  1302  ad5ant25  1303  ad5ant235  1306  ad5ant123  1307  ad5ant124  1308  ad5ant134  1310  ad5ant135  1311  lcmfdvdsb  15283  prmgaplem6  15687  islmhm2  18960  dfon2lem8  31417
  Copyright terms: Public domain W3C validator