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  12839  fi1uzind  13524  brfi1indALT  13527  swrdswrdlem  13744  initoeu2lem1  16975  pm2mpf1  20929  mp2pm2mplem4  20939  neindisj2  21253  2ndcdisj  21585  cusgrsize2inds  26695  elwwlks2  27249  clwlkclwwlklem2a4  27282  clwlkclwwlklem2a  27283  erclwwlktr  27316  erclwwlkntr  27381  clwwlknonex2lem2  27440  frgrnbnb  27634  frgrregord013  27772  zerdivemp1x  34225  icceuelpart  42200  lighneallem3  42294  bgoldbtbndlem4  42466  bgoldbtbnd  42467  tgoldbach  42475  nzerooringczr  42859  lindslinindsimp1  43033  ldepspr  43049  nn0sumshdiglemA  43200  nn0sumshdiglemB  43201
  Copyright terms: Public domain W3C validator