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  13752  addmodlteq  13911  fi1uzind  14458  brfi1indALT  14461  swrdswrdlem  14654  2cshwcshw  14776  lcmfdvdsb  16580  initoeu1  17961  initoeu2lem1  17964  initoeu2  17966  termoeu1  17968  upgrwlkdvdelem  28993  spthonepeq  29009  usgr2pthlem  29020  erclwwlktr  29275  erclwwlkntr  29324  3cyclfrgrrn1  29538  frgrnbnb  29546  frgrncvvdeqlem8  29559  frgrreg  29647  frgrregord013  29648  zerdivemp1x  36815  bgoldbtbndlem4  46476  bgoldbtbnd  46477  tgoldbach  46485
  Copyright terms: Public domain W3C validator