MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com3r Unicode version

Theorem com3r 79
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com3.1
Assertion
Ref Expression
com3r

Proof of Theorem com3r
StepHypRef Expression
1 com3.1 . . 3
21com23 78 . 2
32com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com13  80  com3l  81  com14  88  expd  436  mo3OLD  2324  mob  3281  issref  5385  sotri2  5401  sotri3  5402  relresfld  5539  limuni3  6687  poxp  6912  soxp  6913  tz7.49  7129  omwordri  7240  odi  7247  omass  7248  oewordri  7260  nndi  7291  nnmass  7292  r1sdom  8213  tz9.12lem3  8228  cardlim  8374  carduni  8383  alephordi  8476  alephval3  8512  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  axcclem  8858  zorn2lem5  8901  zorn2lem6  8902  axdclem2  8921  alephval2  8968  gruen  9211  grur1a  9218  grothomex  9228  nqereu  9328  distrlem5pr  9426  psslinpr  9430  ltaprlem  9443  suplem1pr  9451  lbreu  10518  fleqceilz  11981  caubnd  13191  algcvga  14208  algfx  14209  gsummatr01lem3  19159  fiinopn  19410  hausnei  19829  hausnei2  19854  cmpsublem  19899  cmpsub  19900  bwthOLD  19911  fcfneii  20538  ppiublem1  23477  nb3graprlem1  24451  cusgrasize2inds  24477  wlkdvspthlem  24609  usgra2wlkspth  24621  clwwlkprop  24770  clwwlkgt0  24771  clwlkisclwwlklem1  24787  clwwlkf  24794  vdgn1frgrav2  25026  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgraregord013  25118  chintcli  26249  h1datomi  26499  strlem3a  27171  hstrlem3a  27179  mdexchi  27254  cvbr4i  27286  mdsymlem4  27325  mdsymlem6  27327  3jaodd  29091  frr3g  29386  ifscgr  29694  wepwsolem  30987  ldepspr  33074  ad5ant23  33236  ad5ant24  33237  ad5ant25  33238  ee233  33289  rp-fakeimass  37736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator