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  13823  addmodlteq  13984  fi1uzind  14543  brfi1indALT  14546  swrdswrdlem  14739  2cshwcshw  14861  lcmfdvdsb  16677  initoeu1  18065  initoeu2lem1  18068  initoeu2  18070  termoeu1  18072  upgrwlkdvdelem  29769  spthonepeq  29785  usgr2pthlem  29796  erclwwlktr  30051  erclwwlkntr  30100  3cyclfrgrrn1  30314  frgrnbnb  30322  frgrncvvdeqlem8  30335  frgrreg  30423  frgrregord013  30424  zerdivemp1x  37934  bgoldbtbndlem4  47733  bgoldbtbnd  47734  tgoldbach  47742
  Copyright terms: Public domain W3C validator