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  13826  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14742  initoeu2lem1  18059  nzerooringczr  21491  pm2mpf1  22805  mp2pm2mplem4  22815  neindisj2  23131  2ndcdisj  23464  cusgrsize2inds  29471  elwwlks2  29986  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  erclwwlktr  30041  erclwwlkntr  30090  clwwlknonex2lem2  30127  frgrnbnb  30312  frgrregord013  30414  zerdivemp1x  37954  icceuelpart  47423  lighneallem3  47594  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgoldbach  47804  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  lindslinindsimp1  48374  ldepspr  48390  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541
  Copyright terms: Public domain W3C validator