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  ad5ant13OLD  759  ad5ant14OLD  761  ad5ant15OLD  763  ad5ant23OLD  765  ad5ant24OLD  767  ad5ant25OLD  769  ad5ant235OLD  1468  ad5ant123OLD  1470  ad5ant124OLD  1472  ad5ant134OLD  1476  ad5ant135OLD  1478  lcmfdvdsb  15571  prmgaplem6  15973  islmhm2  19241  dfon2lem8  32013
  Copyright terms: Public domain W3C validator