MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com25 Structured version   Visualization version   GIF version

Theorem com25 99
Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 96. (Contributed by Jeff Hankins, 28-Jun-2009.)
Hypothesis
Ref Expression
com5.1 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
Assertion
Ref Expression
com25 (𝜑 → (𝜏 → (𝜒 → (𝜃 → (𝜓𝜂)))))

Proof of Theorem com25
StepHypRef Expression
1 com5.1 . . . 4 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
21com24 95 . . 3 (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏𝜂)))))
32com45 97 . 2 (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓𝜂)))))
43com24 95 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  fi1uzind  13845  brfi1indALT  13848  swrdswrdlem  14056  initoeu2lem1  17264  pm2mpf1  21337  mp2pm2mplem4  21347  neindisj2  21661  2ndcdisj  21994  cusgrsize2inds  27163  elwwlks2  27673  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  erclwwlktr  27728  erclwwlkntr  27778  clwwlknonex2lem2  27815  frgrnbnb  28000  frgrregord013  28102  zerdivemp1x  35108  icceuelpart  43443  lighneallem3  43619  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgoldbach  43829  nzerooringczr  44241  lindslinindsimp1  44410  ldepspr  44426  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator