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  12583  fi1uzind  13274  brfi1indALT  13277  fi1uzindOLD  13280  brfi1indALTOLD  13283  swrdswrdlem  13453  initoeu2lem1  16658  pm2mpf1  20598  mp2pm2mplem4  20608  neindisj2  20921  2ndcdisj  21253  cusgrsize2inds  26343  elwwlks2  26855  clwlkclwwlklem2a4  26892  clwlkclwwlklem2a  26893  erclwwlkstr  26929  erclwwlksntr  26941  frgrnbnb  27150  frgrregord013  27237  zerdivemp1x  33726  icceuelpart  41142  lighneallem3  41295  bgoldbtbndlem4  41467  bgoldbtbnd  41468  tgoldbach  41476  tgoldbachOLD  41483  nzerooringczr  41843  lindslinindsimp1  42017  ldepspr  42033  nn0sumshdiglemA  42184  nn0sumshdiglemB  42185
  Copyright terms: Public domain W3C validator