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  13748  addmodlteq  13907  fi1uzind  14454  brfi1indALT  14457  swrdswrdlem  14650  2cshwcshw  14772  lcmfdvdsb  16576  initoeu1  17957  initoeu2lem1  17960  initoeu2  17962  termoeu1  17964  upgrwlkdvdelem  28982  spthonepeq  28998  usgr2pthlem  29009  erclwwlktr  29264  erclwwlkntr  29313  3cyclfrgrrn1  29527  frgrnbnb  29535  frgrncvvdeqlem8  29548  frgrreg  29636  frgrregord013  29637  zerdivemp1x  36803  bgoldbtbndlem4  46462  bgoldbtbnd  46463  tgoldbach  46471
  Copyright terms: Public domain W3C validator