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  13219  fi1uzind  13920  brfi1indALT  13923  swrdswrdlem  14126  initoeu2lem1  17353  pm2mpf1  21512  mp2pm2mplem4  21522  neindisj2  21836  2ndcdisj  22169  cusgrsize2inds  27355  elwwlks2  27864  clwlkclwwlklem2a4  27894  clwlkclwwlklem2a  27895  erclwwlktr  27919  erclwwlkntr  27968  clwwlknonex2lem2  28005  frgrnbnb  28190  frgrregord013  28292  zerdivemp1x  35699  icceuelpart  44370  lighneallem3  44541  bgoldbtbndlem4  44742  bgoldbtbnd  44743  tgoldbach  44751  nzerooringczr  45112  lindslinindsimp1  45280  ldepspr  45296  nn0sumshdiglemA  45447  nn0sumshdiglemB  45448
 Copyright terms: Public domain W3C validator