Theorem com4l 92

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.)

Hypothesis

Ref	Expression
com4.1	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Assertion

Ref	Expression
com4l	|- ( ps -> ( ch -> ( th -> ( ph -> ta ) ) ) )

Proof of Theorem com4l

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	com3l 89	. 2 |- ( ps -> ( ch -> ( ph -> ( th -> ta ) ) ) )
3	2	com34 91	1 |- ( ps -> ( ch -> ( th -> ( ph -> 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:  com4t  93  com4r  94  com14  96  com5l  100  3impd  1281  merco2  1661  onint  6995  oalimcl  7640  oeordsuc  7674  fisup2g  8374  fiinf2g  8406  zorn2lem7  9324  inar1  9597  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  expnbnd  12993  facwordi  13076  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  unbenlem  15612  fiinopn  20706  cmpsublem  21202  dvcnvrelem1  23780  axcontlem4  25847  axcont  25856  spansncol  28427  atcvat4i  29256  sumdmdlem  29277  nocvxminlem  31893  broutsideof2  32229  relowlpssretop  33212  cvrat4  34729  pm2.43cbi  38724