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  12703  addmodlteq  12860  fi1uzind  13392  brfi1indALT  13395  swrdswrdlem  13580  2cshwcshw  13692  lcmfdvdsb  15479  initoeu1  16783  initoeu2lem1  16786  initoeu2  16788  termoeu1  16790  upgrwlkdvdelem  26763  spthonepeq  26779  usgr2pthlem  26790  erclwwlktr  27066  erclwwlkntr  27123  3cyclfrgrrn1  27360  frgrnbnb  27368  frgrncvvdeqlem8  27381  frgrreg  27483  frgrregord013  27484  zerdivemp1x  33978  bgoldbtbndlem4  42123  bgoldbtbnd  42124  tgoldbach  42132  tgoldbachOLD  42139
 Copyright terms: Public domain W3C validator