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  6590  nnmordi  6789  fundmen  7094  fiintim  7238  elfzodifsumelfzo  10619  ssfzo12  10642  swrdswrdlem  11476  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  dvdsmodexp  12562  dvdsaddre2b  12608  infpnlem1  13138  grpinveu  13843  mulgass2  14363  lss1d  14720  cnpnei  15320  clwwlkccatlem  16641