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  13147  addmodlteq  13304  fi1uzind  13845  brfi1indALT  13848  swrdswrdlem  14056  2cshwcshw  14177  lcmfdvdsb  15977  initoeu1  17261  initoeu2lem1  17264  initoeu2  17266  termoeu1  17268  upgrwlkdvdelem  27445  spthonepeq  27461  usgr2pthlem  27472  erclwwlktr  27728  erclwwlkntr  27778  3cyclfrgrrn1  27992  frgrnbnb  28000  frgrncvvdeqlem8  28013  frgrreg  28101  frgrregord013  28102  zerdivemp1x  35108  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgoldbach  43829
  Copyright terms: Public domain W3C validator