Theorem com24 87

Description: Commutation of antecedents. Swap 2nd and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com4.1	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Assertion

Ref	Expression
com24	|- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) )

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	com4t 85	. 2 |- ( ch -> ( th -> ( ph -> ( ps -> ta ) ) ) )
3	2	com13 80	1 |- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com25  91  tfrlem9  6580  nnmordi  6779  fundmen  7084  fiintim  7228  elfzodifsumelfzo  10597  ssfzo12  10620  swrdswrdlem  11454  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  dvdsmodexp  12540  dvdsaddre2b  12586  infpnlem1  13116  grpinveu  13820  mulgass2  14336  lss1d  14692  cnpnei  15243  clwwlkccatlem  16555