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  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