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  6428  nnmordi  6625  fundmen  6922  fiintim  7054  elfzodifsumelfzo  10367  ssfzo12  10390  swrdswrdlem  11195  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  dvdsmodexp  12221  dvdsaddre2b  12267  infpnlem1  12797  grpinveu  13485  mulgass2  13935  lss1d  14260  cnpnei  14806