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  12911  addmodlteq  13068  fi1uzind  13597  brfi1indALT  13600  swrdswrdlem  13817  2cshwcshw  13980  lcmfdvdsb  15766  initoeu1  17050  initoeu2lem1  17053  initoeu2  17055  termoeu1  17057  upgrwlkdvdelem  27092  spthonepeq  27108  usgr2pthlem  27119  erclwwlktr  27415  erclwwlkntr  27473  3cyclfrgrrn1  27697  frgrnbnb  27705  frgrncvvdeqlem8  27718  frgrreg  27830  frgrregord013  27831  zerdivemp1x  34375  bgoldbtbndlem4  42731  bgoldbtbnd  42732  tgoldbach  42740
  Copyright terms: Public domain W3C validator