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  6471  nnmordi  6670  fundmen  6967  fiintim  7104  elfzodifsumelfzo  10419  ssfzo12  10442  swrdswrdlem  11252  swrdswrd  11253  wrd2ind  11271  swrdccatin1  11273  dvdsmodexp  12322  dvdsaddre2b  12368  infpnlem1  12898  grpinveu  13587  mulgass2  14037  lss1d  14363  cnpnei  14909  clwwlkccatlem  16143