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  12796  addmodlteq  12953  fi1uzind  13481  brfi1indALT  13484  swrdswrdlem  13668  2cshwcshw  13780  lcmfdvdsb  15564  initoeu1  16868  initoeu2lem1  16871  initoeu2  16873  termoeu1  16875  upgrwlkdvdelem  26867  spthonepeq  26883  usgr2pthlem  26894  erclwwlktr  27172  erclwwlkntr  27229  3cyclfrgrrn1  27467  frgrnbnb  27475  frgrncvvdeqlem8  27488  frgrreg  27593  frgrregord013  27594  zerdivemp1x  34078  bgoldbtbndlem4  42224  bgoldbtbnd  42225  tgoldbach  42233  tgoldbachOLD  42240
  Copyright terms: Public domain W3C validator