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

Step	Hyp	Ref	Expression
1		com5.1	. . . 4 |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
2	1	com24 87	. . 3 |- ( ph -> ( th -> ( ch -> ( ps -> ( ta -> et ) ) ) ) )
3	2	com45 89	. 2 |- ( ph -> ( th -> ( ch -> ( ta -> ( ps -> et ) ) ) ) )
4	3	com24 87	1 |- ( ph -> ( ta -> ( ch -> ( th -> ( ps -> et ) ) ) ) )

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