Theorem com4l 84

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

Assertion

Ref	Expression
com4l

Proof of Theorem com4l

Step	Hyp	Ref	Expression
1		com4.1	. . 3
2	1	com3l 81	. 2
3	2	com34 83	1

Syntax hints:  ->wi 4

This theorem is referenced by:  com4t  85  com4r  86  com14  88  com5l  92  3impd  1210  merco2  1569  onint  6630  oalimcl  7228  oeordsuc  7262  fisup2g  7947  zorn2lem7  8903  inar1  9174  rpnnen1lem5  11241  expnbnd  12295  facwordi  12367  brfi1uzind  12532  unbenlem  14426  fiinopn  19410  cmpsublem  19899  bwthOLD  19911  dvcnvrelem1  22418  axcontlem4  24270  axcont  24279  spansncol  26486  atcvat4i  27316  sumdmdlem  27337  nocvxminlem  29450  broutsideof2  29772  pm2.43cbi  33288  cvrat4  35167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7