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  13759  fi1uzind  14465  brfi1indALT  14468  swrdswrdlem  14661  initoeu2lem1  17974  nzerooringczr  21340  pm2mpf1  22621  mp2pm2mplem4  22631  neindisj2  22947  2ndcdisj  23280  cusgrsize2inds  29143  elwwlks2  29653  clwlkclwwlklem2a4  29683  clwlkclwwlklem2a  29684  erclwwlktr  29708  erclwwlkntr  29757  clwwlknonex2lem2  29794  frgrnbnb  29979  frgrregord013  30081  zerdivemp1x  37279  icceuelpart  46563  lighneallem3  46734  bgoldbtbndlem4  46935  bgoldbtbnd  46936  tgoldbach  46944  lindslinindsimp1  47300  ldepspr  47316  nn0sumshdiglemA  47467  nn0sumshdiglemB  47468
  Copyright terms: Public domain W3C validator