MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com25 Structured version   Visualization version   GIF version

Theorem com25 97
Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 94. (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 93 . . 3 (𝜑 → (𝜃 → (𝜒 → (𝜓 → (𝜏𝜂)))))
32com45 95 . 2 (𝜑 → (𝜃 → (𝜒 → (𝜏 → (𝜓𝜂)))))
43com24 93 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  12450  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdswrdlem  13311  initoeu2lem1  16487  pm2mpf1  20423  mp2pm2mplem4  20433  neindisj2  20737  2ndcdisj  21069  usgrafisinds  25942  cusgrasize2inds  26005  usgra2wlkspthlem1  26147  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  erclwwlktr  26343  erclwwlkntr  26355  rusgrasn  26472  frgranbnb  26547  vdn0frgrav2  26550  vdn1frgrav2  26552  frgrawopreg  26576  frgrareg  26644  frgraregord013  26645  zerdivemp1x  32916  icceuelpart  39974  lighneallem3  40062  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  cusgrsize2inds  40669  uspgrn2crct  41011  elwwlks2  41170  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  erclwwlkstr  41243  erclwwlksntr  41255  frgrnbnb  41463  frgrwopreg  41486  av-frgraregord013  41549  nzerooringczr  41864  lindslinindsimp1  42040  ldepspr  42056  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator