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

Theorem com25 91
Description: Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
Hypothesis
Ref Expression
com5.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
Assertion
Ref Expression
com25  |-  ( ph  ->  ( ta  ->  ( ch  ->  ( th  ->  ( ps  ->  et )
) ) ) )

Proof of Theorem com25
StepHypRef Expression
1 com5.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
21com24 87 . . 3  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ps  ->  ( ta  ->  et )
) ) ) )
32com45 89 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ta  ->  ( ps  ->  et )
) ) ) )
43com24 87 1  |-  ( ph  ->  ( ta  ->  ( ch  ->  ( th  ->  ( ps  ->  et )
) ) ) )
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  11873  brfi1uzind  12486  swrdswrdlem  12645  initoeu2lem1  15507  pm2mpf1  19482  mp2pm2mplem4  19492  neindisj2  19807  2ndcdisj  20139  usgrafisinds  24712  cusgrasize2inds  24776  usgra2wlkspthlem1  24918  clwlkisclwwlklem2a4  25083  clwlkisclwwlklem2a  25084  erclwwlktr  25114  erclwwlkntr  25126  rusgrasn  25244  frgranbnb  25319  vdn0frgrav2  25322  vdn1frgrav2  25324  frgrawopreg  25348  frgrareg  25416  frgraregord013  25417  zerdivemp1  25731  zerdivemp1x  31604  icceuelpart  37666  nzerooringczr  38324  lindslinindsimp1  38502  ldepspr  38518  nn0sumshdiglemA  38684  nn0sumshdiglemB  38685
  Copyright terms: Public domain W3C validator