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

Theorem com3l 81
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1
Assertion
Ref Expression
com3l

Proof of Theorem com3l
StepHypRef Expression
1 com3.1 . . 3
21com3r 79 . 2
32com3r 79 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com4l  84  impd  431  expdcom  439  rexlimdv  2947  prel12  4207  reusv3  4660  sotri2  5401  relcoi1  5541  isofrlem  6236  oprabid  6323  sorpsscmpl  6591  tfindsg  6695  frxp  6910  poxp  6912  reldmtpos  6982  tfrlem9  7073  tfr3  7087  oawordri  7218  odi  7247  omass  7248  undifixp  7525  isinf  7753  pssnn  7758  ordiso2  7961  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  indcardi  8443  dfac2  8532  cfslb2n  8669  infpssrlem4  8707  axdc4lem  8856  zorn2lem7  8903  fpwwe2lem8  9036  grudomon  9216  distrlem5pr  9426  ltexprlem1  9435  axpre-sup  9567  bndndx  10819  uzind2  10980  difreicc  11681  elfznelfzo  11915  ssnn0fi  12094  leexp1a  12224  swrdswrdlem  12684  swrdswrd  12685  swrdccat3blem  12720  unbenlem  14426  infpnlem1  14428  mndassOLD  15932  ring1ne0  17239  neindisj2  19624  cmpsub  19900  bwthOLD  19911  usgrafisinds  24413  wlkdvspth  24610  usgrcyclnl2  24641  wwlknred  24723  wwlkm1edg  24735  wlklenvclwlk  24839  el2spthonot  24870  2spontn0vne  24887  hashnbgravdg  24913  frgra3vlem1  25000  3vfriswmgralem  25004  vdn0frgrav2  25023  frgrawopreglem4  25047  numclwwlkovf2ex  25086  grpomndo  25348  rngoueqz  25432  rngoridfz  25437  shscli  26235  mdbr3  27216  mdbr4  27217  dmdbr3  27224  dmdbr4  27225  mdslmd1i  27248  chjatom  27276  mdsymlem4  27325  cdj3lem2b  27356  3jaodd  29091  dfon2lem6  29220  poseq  29333  nocvxminlem  29450  funray  29790  imp5p  30129  brabg2  30206  neificl  30246  subsubelfzo0  32338  fzoopth  32340  2ffzoeq  32341  usgra2pth  32354  initoeu1  32617  termoeu1  32624  ztprmneprm  32936  eel12131  33506  eel32131  33509  3imp231  33615  bnj517  33943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator