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  6465  nnmordi  6662  fundmen  6959  fiintim  7093  elfzodifsumelfzo  10407  ssfzo12  10430  swrdswrdlem  11236  swrdswrd  11237  wrd2ind  11255  swrdccatin1  11257  dvdsmodexp  12306  dvdsaddre2b  12352  infpnlem1  12882  grpinveu  13571  mulgass2  14021  lss1d  14347  cnpnei  14893