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  13793  addmodlteq  13952  fi1uzind  14502  brfi1indALT  14505  swrdswrdlem  14698  2cshwcshw  14820  lcmfdvdsb  16630  initoeu1  18019  initoeu2lem1  18022  initoeu2  18024  termoeu1  18026  upgrwlkdvdelem  29642  spthonepeq  29658  usgr2pthlem  29669  erclwwlktr  29924  erclwwlkntr  29973  3cyclfrgrrn1  30187  frgrnbnb  30195  frgrncvvdeqlem8  30208  frgrreg  30296  frgrregord013  30297  zerdivemp1x  37571  bgoldbtbndlem4  47290  bgoldbtbnd  47291  tgoldbach  47299
  Copyright terms: Public domain W3C validator