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  11758  brfi1uzind  12340  swrdswrdlem  12474  neindisj2  18862  2ndcdisj  19195  usgrafisinds  23498  cusgrasize2inds  23557  zerdivemp1  24093  zerdivemp1x  28929  usgra2wlkspthlem1  30464  clwlkisclwwlklem2a4  30614  clwlkisclwwlklem2a  30615  erclwwlktr  30653  erclwwlkntr  30669  rusgrasn  30725  frgranbnb  30780  vdn0frgrav2  30784  vdn1frgrav2  30786  frgrawopreg  30810  frgrareg  30878  frgraregord013  30879  scmatsubcl  31083  scmatmulcl  31085  lindslinindsimp1  31143  ldepspr  31159  pm2mpf1  31306  mp2pm2mplem4  31316
  Copyright terms: Public domain W3C validator