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  12536  addmodlteq  12693  fi1uzind  13226  brfi1indALT  13229  fi1uzindOLD  13232  brfi1indALTOLD  13235  swrdswrdlem  13405  2cshwcshw  13516  lcmfdvdsb  15291  initoeu1  16593  initoeu2lem1  16596  initoeu2  16598  termoeu1  16600  upgrwlkdvdelem  26518  spthonepeq  26534  usgr2pthlem  26545  erclwwlkstr  26819  erclwwlksntr  26831  3cyclfrgrrn1  27030  frgrnbnb  27038  frgrncvvdeqlemB  27052  numclwwlkovf2ex  27092  frgrreg  27123  frgrregord013  27124  zerdivemp1x  33413  bgoldbtbndlem4  41011  bgoldbtbnd  41012  tgoldbach  41019  tgoldbachOLD  41026
 Copyright terms: Public domain W3C validator