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

Theorem com15 101
Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
Hypothesis
Ref Expression
com5.1 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
Assertion
Ref Expression
com15 (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑𝜂)))))

Proof of Theorem com15
StepHypRef Expression
1 com5.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
21com5l 100 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑𝜂)))))
32com4r 94 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:  injresinjlem  13140  addmodlteq  13297  fi1uzind  13839  brfi1indALT  13842  swrdswrdlem  14045  2cshwcshw  14166  lcmfdvdsb  15964  initoeu1  17249  initoeu2lem1  17252  initoeu2  17254  termoeu1  17256  upgrwlkdvdelem  27503  spthonepeq  27519  usgr2pthlem  27530  erclwwlktr  27785  erclwwlkntr  27834  3cyclfrgrrn1  28048  frgrnbnb  28056  frgrncvvdeqlem8  28069  frgrreg  28157  frgrregord013  28158  zerdivemp1x  35265  bgoldbtbndlem4  44120  bgoldbtbnd  44121  tgoldbach  44129
  Copyright terms: Public domain W3C validator