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  12628  fi1uzind  13317  brfi1indALT  13320  swrdswrdlem  13505  initoeu2lem1  16711  pm2mpf1  20652  mp2pm2mplem4  20662  neindisj2  20975  2ndcdisj  21307  cusgrsize2inds  26405  elwwlks2  26933  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  erclwwlktr  26979  erclwwlkntr  27035  clwwlknonex2lem2  27083  frgrnbnb  27273  frgrregord013  27382  zerdivemp1x  33876  icceuelpart  41697  lighneallem3  41849  bgoldbtbndlem4  42021  bgoldbtbnd  42022  tgoldbach  42030  tgoldbachOLD  42037  nzerooringczr  42397  lindslinindsimp1  42571  ldepspr  42587  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator