Theorem com4r 86

Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1

Assertion

Ref	Expression
com4r

Proof of Theorem com4r

Step	Hyp	Ref	Expression
1		com4.1	. . 3
2	1	com4t 85	. 2
3	2	com4l 84	1

Syntax hints:  ->wi 4

This theorem is referenced by:  com15  93  3expd  1213  elpwunsn  4070  onint  6630  tfindsg  6695  findsg  6727  tfrlem9  7073  tz7.49  7129  oaordi  7214  odi  7247  nnaordi  7286  nndi  7291  php  7721  fiint  7817  carduni  8383  dfac2  8532  axcclem  8858  zorn2lem6  8902  zorn2lem7  8903  grur1a  9218  mulcanpi  9299  ltexprlem7  9441  axpre-sup  9567  xrsupsslem  11527  xrinfmsslem  11528  supxrunb1  11540  supxrunb2  11541  mulgnnass  16170  fiinopn  19410  bwthOLD  19911  axcont  24279  sumdmdlem  27337  eel32131  33509  ee33VD  33679

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