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

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com25  91  tfrlem9  6594  nnmordi  6793  fundmen  7098  fiintim  7242  elfzodifsumelfzo  10636  ssfzo12  10659  swrdswrdlem  11498  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  dvdsmodexp  12587  dvdsaddre2b  12633  infpnlem1  13167  grpinveu  13902  mulgass2  14470  lss1d  14829  cnpnei  15445  clwwlkccatlem  16846