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  13011  fi1uzind  13705  brfi1indALT  13708  swrdswrdlem  13906  initoeu2lem1  17107  pm2mpf1  21095  mp2pm2mplem4  21105  neindisj2  21419  2ndcdisj  21752  cusgrsize2inds  26922  elwwlks2  27431  clwlkclwwlklem2a4  27461  clwlkclwwlklem2a  27462  erclwwlktr  27486  erclwwlkntr  27536  clwwlknonex2lem2  27573  frgrnbnb  27760  frgrregord013  27862  zerdivemp1x  34778  icceuelpart  43100  lighneallem3  43276  bgoldbtbndlem4  43477  bgoldbtbnd  43478  tgoldbach  43486  nzerooringczr  43843  lindslinindsimp1  44014  ldepspr  44030  nn0sumshdiglemA  44182  nn0sumshdiglemB  44183
  Copyright terms: Public domain W3C validator