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

Theorem syl5eqel 2515
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqel.1  |-  A  =  B
syl5eqel.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
syl5eqel  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3  |-  A  =  B
21a1i 11 . 2  |-  ( ph  ->  A  =  B )
3 syl5eqel.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2511 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    e. wcel 1869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-cleq 2415  df-clel 2418
This theorem is referenced by:  syl5eqelr  2516  3eltr4g  2529  csbexg  4556  rabexd  4574  snex  4660  otel3xp  4887  dmresexg  5144  riotaprop  6288  elovimad  6343  fovrn  6451  fnovrn  6456  ovima0  6460  f1oabexg  6764  cofunexg  6769  cofunex2g  6770  abrexex2g  6782  xpexgALT  6798  el2xptp0  6849  opiota  6864  fnwelem  6920  mptsuppdifd  6946  fvmpt2curryd  7024  tfrlem12  7113  rdgseg  7146  oelim2  7302  oeeulem  7308  ecexg  7373  qsexg  7427  pmex  7483  resixpfo  7566  elixpsn  7567  unxpdomlem3  7782  rabfi  7800  fnfi  7853  rnfi  7861  iunfi  7866  unifi  7867  pwfilem  7872  fsuppun  7906  fsuppcolem  7918  mapfienlem2  7923  supexd  7971  infexd  8003  infcl  8008  fiinfcl  8021  cantnfp1lem1  8186  oemapvali  8192  wemapwe  8205  cnfcomlem  8207  cnfcom  8208  cnfcom2lem  8209  cnfcom2  8210  cnfcom3lem  8211  cnfcom3  8212  prwf  8285  scott0  8360  htalem  8370  infxpenlem  8447  dfac8b  8464  cfss  8697  cofsmo  8701  coftr  8705  fin1a2lem10  8841  hsmexlem4  8861  hsmex2  8865  fpwwe  9073  canthwelem  9077  pwfseqlem1  9085  wuntp  9138  wunsn  9143  wunsuc  9144  wunr1om  9146  wunot  9150  r1limwun  9163  tsk1  9191  tsk2  9192  tskr1om  9194  gruuni  9227  grusn  9231  gruina  9245  wuncn  9596  negcl  9877  peano5nni  10614  peano5uzi  11026  quoremz  12083  quoremnn0  12084  quoremnn0ALT  12085  intfrac2  12086  intfracq  12087  fsuppmapnn0fiublem  12203  fsuppmapnn0fiub  12204  seqf1olem1  12253  seqf1olem2  12254  serle  12269  discr1  12409  swrdccatin2  12839  swrdccatin12lem2  12841  swrdccatin12  12843  swrdccat3  12844  swrdccat3a  12846  cats1cld  12947  sqrlem4  13303  sqreulem  13416  reccn2  13653  fsumzcl2  13797  fsummsnunz  13808  fsump1i  13823  fsumabs  13854  o1fsum  13866  supcvg  13907  mertenslem1  13933  mertenslem2  13934  fprodcllemf  14005  rpnnen2  14271  ruclem12  14286  bitsfzolem  14400  bitsfzolemOLD  14401  bezoutlem2OLD  14497  bezoutlem2  14500  algrf  14525  algcvg  14528  algcvga  14531  algfx  14532  eucalgcvga  14538  eucalg  14539  lcmscllemOLD  14575  absprodnn  14581  prmdiv  14726  pythagtriplem11  14768  pythagtriplem13  14770  pcprecl  14782  infpnlem1  14847  infpnlem2  14848  4sqlem5  14879  mul4sqlem  14890  4sqlem13OLD  14894  4sqlem14OLD  14895  4sqlem17OLD  14898  4sqlem18OLD  14899  4sqlem13  14900  4sqlem14  14901  4sqlem17  14904  4sqlem18  14905  vdwlem5  14928  wunndx  15130  wunress  15182  1strwunbndx  15221  restid  15325  mreexdomd  15548  acsfn0  15559  acsfn1  15560  acsfn2  15562  rcaninv  15692  funcf2  15766  funcpropd  15798  fthepi  15826  ressffth  15836  elhomai2  15922  catcxpccl  16085  diag1cl  16120  yonedalem1  16150  prdsinvlem  16787  subggrp  16813  nsgacs  16846  ghmima  16896  gimco  16925  gicref  16928  cntrnsg  16988  oppgmnd  16998  cayley  17048  symgfixfolem1  17072  pmtrdifellem1  17110  psgndmsubg  17136  efgredlemf  17384  efgredlemd  17387  efgredlemc  17388  cycsubgcyg  17528  gsumzaddlem  17547  gsum2dlem1  17595  gsum2dlem2  17596  dprdfid  17643  dprd2dlem1  17667  dprd2da  17668  ablfacrplem  17691  ablfacrp  17692  ablfacrp2  17693  ablfac1lem  17694  pgpfac1lem1  17700  pgpfac1lem2  17701  pgpfac1lem3a  17702  pgpfac1lem3  17703  pgpfac1lem4  17704  pgpfac1lem5  17705  pgpfaclem1  17707  ablfaclem3  17713  opprring  17852  subrgring  18004  lmhmkerlss  18267  rlmlmod  18421  lidl0cl  18428  lidlacl  18429  lidlnegcl  18430  lidlmcl  18434  lidlacs  18438  fidomndrnglem  18523  gsumbagdiag  18593  psrass1lem  18594  psrlidm  18620  psrridm  18621  mplsubrglem  18656  vr1cl2  18779  vr1cl  18803  subrgvr1cl  18848  coe1fzgsumdlem  18888  evl1rhm  18913  evl1gsumdlem  18937  zringlpirlem2OLD  19046  zringlpirlem3OLD  19047  zringlpirlem2  19048  zringlpirlem3  19049  cygznlem1  19129  cygznlem2a  19130  cygznlem3  19132  isphld  19213  lindsmm  19378  mpt2matmul  19463  scmatscmiddistr  19525  scmatf  19546  1marepvmarrepid  19592  1marepvsma1  19600  mdetleib2  19605  smadiadetlem3  19685  cramerimplem1  19700  cramerimplem2  19701  cramerimplem3  19702  cramerimp  19703  pmatcollpwscmatlem2  19806  pmatcollpwscmat  19807  mp2pm2mplem4  19825  chmatcl  19844  cpmidgsum  19884  cpmidgsumm2pm  19885  cpmidpmatlem2  19887  cpmidpmatlem3  19888  chcoeffeqlem  19901  cayhamlem3  19903  topopn  19928  rintopn  19931  fctop  20011  topcld  20042  intcld  20047  uncld  20048  unicld  20053  mretopd  20100  neiptoptop  20139  tgrest  20167  restin  20174  neitr  20188  restcls  20189  restntr  20190  restlp  20191  restperf  20192  perfopn  20193  ordtbaslem  20196  ordtuni  20198  ordtbas2  20199  ordtbas  20200  ordttopon  20201  ordtopn1  20202  ordtopn2  20203  ordtrest2lem  20211  ordtrest2  20212  cnco  20274  cnrest  20293  cnprest2  20298  lmss  20306  cncmp  20399  imacmp  20404  fiuncmp  20411  concompcon  20439  cldllycmp  20502  hausmapdom  20507  lfinun  20532  locfindis  20537  kgentopon  20545  1stckgen  20561  ptbasin  20584  ptbasfi  20588  pttopon  20603  xkotopon  20607  txbasval  20613  ptpjcn  20618  ptcldmpt  20621  dfac14lem  20624  txcn  20633  ptcn  20634  ptrescn  20646  txkgen  20659  cnmpt12f  20673  xkofvcn  20691  qtopval2  20703  elqtop  20704  qtoptop2  20706  hmeoco  20779  idhmeo  20780  ordthmeolem  20808  ptunhmeo  20815  xkohmeo  20822  qtopf1  20823  cfinfil  20900  ufprim  20916  ufildr  20938  fin1aufil  20939  fmfg  20956  elfm3  20957  fbflim  20983  flimclslem  20991  flffbas  21002  cnpflf2  21007  flfcnp2  21014  fclsbas  21028  alexsublem  21051  ptcmplem3  21061  ptcmpg  21064  cnextcn  21074  tgpsubcn  21097  tmdgsum  21102  symgtgp  21108  tmdlactcn  21109  submtmd  21111  clssubg  21115  qustgplem  21127  prdstmdd  21130  tsmsfbas  21134  eltsms  21139  tsmssubm  21149  dvrcn  21190  utop2nei  21257  utop3cls  21258  utopreg  21259  blres  21438  prdsbl  21498  metrest  21531  metustexhalf  21563  subgngp  21635  nlmvscnlem2  21680  nlmvscnlem1  21681  nrginvrcnlem  21685  qtopbaslem  21771  tgqioo  21810  icccmplem2  21833  icccmp  21835  reconnlem2  21837  xrge0tsms  21844  nmcn  21854  metnrmlem2  21869  metnrmlem2OLD  21884  divcn  21892  fsumcn  21894  fsum2cn  21895  cncfmet  21932  addccncf  21940  cnmpt2pc  21948  icchmeo  21961  cnrehmeo  21973  cnheiborlem  21974  bndth  21978  lebnumlem2  21982  lebnumlem2OLD  21985  htpycom  21999  htpyid  22000  htpyco1  22001  htpycc  22003  reparphti  22020  pcohtpylem  22042  pcoptcl  22044  pcoass  22047  pcorevcl  22048  pcorevlem  22049  ipcnlem2  22207  ipcnlem1  22208  cmsss  22310  minveclem4c  22359  minveclem3b  22362  minveclem4a  22364  minveclem4  22366  minveclem6  22368  minveclem4cOLD  22371  minveclem3bOLD  22374  minveclem4aOLD  22376  minveclem4OLD  22378  minveclem6OLD  22380  pjthlem1  22383  ivthlem2  22395  ivthlem3  22396  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  finiunmbl  22489  voliunlem1  22495  ioombl1lem1  22503  ioombl1lem3  22505  ioombl1lem4  22506  ovolioo  22513  opnmblALT  22553  mbfimaicc  22581  mbfid  22584  mbfeqalem  22590  mbfres  22592  cncombf  22606  mbfi1flim  22673  itg2monolem2  22701  itg2monolem3  22702  itg2mono  22703  itg2cnlem1  22711  itgcl  22733  iblss  22754  itgeqa  22763  itgss3  22764  itgless  22766  iblconst  22767  ibladdlem  22769  itgaddlem1  22772  iblabslem  22777  iblabsr  22779  iblmulc2  22780  itggt0  22791  itgcn  22792  limcvallem  22818  limcflflem  22827  limcres  22833  cnplimc  22834  limccnp  22838  limccnp2  22839  dvreslem  22856  dvres2lem  22857  dvcnp  22865  dvnff  22869  dvmptres2  22908  dvmptres  22909  dvmptntr  22917  dvmptfsum  22919  dvcnvlem  22920  dvcnv  22921  dvferm1lem  22928  dvferm2lem  22930  dvlipcn  22938  dvlip2  22939  c1liplem1  22940  lhop1lem  22957  dvcnvrelem2  22962  dvcvx  22964  dvfsumge  22966  dvfsumlem3  22972  ftc1lem3  22982  ftc1lem4  22983  mdegleb  23005  ply1remlem  23105  ply0  23154  plyid  23155  plyeq0lem  23156  dgrub  23180  dgrub2  23181  dgrlb  23182  coeidlem  23183  coeaddlem  23195  coemullem  23196  coemulhi  23200  dgreq0  23211  dgrlt  23212  dgradd2  23214  dgrmul  23216  dgrcolem2  23220  dgrco  23221  plycj  23223  coecj  23224  plydivlem2  23239  plydivlem4  23241  plyremlem  23249  plyrem  23250  quotcan  23254  vieta1lem1  23255  elqaalem2  23265  elqaalem3  23266  elqaalem2OLD  23268  elqaalem3OLD  23269  radcnvcl  23364  psercnlem1  23372  pserdvlem2  23375  pilem2  23399  pilem2OLD  23400  pilem3  23401  pilem3OLD  23402  efabl  23491  efsubm  23492  logfac  23542  logcnlem2  23580  logcnlem3  23581  logcnlem4  23582  dvlog  23588  cxpcn  23677  cxpcn3lem  23679  ang180lem1  23730  ang180lem2  23731  ang180lem3  23732  pythag  23738  heron  23756  quart1lem  23773  xrlimcnp  23886  efrlim  23887  ftalem1  23989  ftalem2  23990  ftalem4  23992  ftalem5  23993  ftalem4OLD  23994  ftalem5OLD  23995  basellem1  23999  basellem2  24000  basellem3  24001  basellem4  24002  basellem5  24003  basellem8  24006  dchr1cl  24171  dchrinvcl  24173  dchrptlem1  24184  dchrptlem2  24185  bposlem3  24206  bposlem5  24208  bposlem6  24209  lgsqrlem2  24262  lgsqrlem3  24263  lgsqrlem4  24264  lgseisenlem1  24269  lgseisenlem2  24270  lgseisenlem3  24271  lgseisenlem4  24272  lgsquadlem1  24274  lgsquadlem2  24275  lgsquadlem3  24276  2sqlem8  24292  chebbnd1lem1  24299  chebbnd1lem2  24300  chebbnd1lem3  24301  mulog2sumlem2  24365  selberglem2  24376  chpdifbndlem1  24383  chpdifbndlem2  24384  pntrmax  24394  pntpbnd1a  24415  pntpbnd1  24416  pntpbnd2  24417  pntibndlem1  24419  pntibndlem2  24421  pntibndlem3  24422  pntlemd  24424  pntlemc  24425  pntlema  24426  pntlemg  24428  pntlemr  24432  pntlemj  24433  ostth2lem2  24464  ostth2lem3  24465  ostth2lem4  24466  ostth2  24467  ostth3  24468  tgelrnln  24667  mirauto  24721  lmiisolem  24830  eleesub  24933  axsegconlem2  24940  axsegconlem8  24946  axlowdimlem7  24970  axlowdimlem17  24980  usgrares1  25130  usgrafilem2  25132  cusgrares  25192  cusgrasizeinds  25196  cusgrafilem3  25201  wlks  25239  trls  25258  hashwwlkext  25466  qerclwwlknfi  25549  hashclwwlkn0  25550  frgrawopreglem1  25764  grpoinvfval  25944  grpodivfval  25962  gxfval  25977  ghgrpOLD  26088  isvc  26192  isnv  26223  imsmet  26315  smcnlem  26325  minvecolem2  26509  minvecolem3  26510  minvecolem4c  26513  minvecolem4  26514  minvecolem5  26515  minvecolem6  26516  minvecolem2OLD  26519  minvecolem3OLD  26520  minvecolem4cOLD  26523  minvecolem4OLD  26524  minvecolem5OLD  26525  minvecolem6OLD  26526  hhssabloi  26905  pjhthlem1  27036  pjoc1i  27076  cnlnadjlem3  27714  cnlnadjlem5  27716  mdsymlem1  28048  mdsymlem3  28050  abrexexd  28136  acunirnmpt  28257  acunirnmpt2  28258  acunirnmpt2f  28259  aciunf1lem  28260  imafi2  28288  gsumle  28543  gsummpt2co  28544  mdetpmtr1  28651  mdetpmtr2  28652  mdetpmtr12  28653  madjusmdetlem1  28655  madjusmdetlem3  28657  ordtconlem1  28732  xrge0pluscn  28748  prsiga  28955  inelsiga  28959  sigapildsys  28986  ldgenpisyslem1  28987  ldgenpisys  28990  inelros  28997  fiunelros  28998  mbfmcst  29083  mbfmco  29088  mbfmcnt  29092  dya2icoseg  29101  fiunelcarsg  29150  carsggect  29152  omsmeas  29157  omsmeasOLD  29158  sibf0  29169  sibff  29171  sibfinima  29174  sibfof  29175  sitgclg  29177  eulerpartlemt  29206  sseqval  29223  0rrv  29286  rrvsum  29289  signsplypnf  29441  signsply0  29442  signsvtn0  29461  signstfveq0a  29467  signstfveq0  29468  signsvtp  29474  signsvtn  29475  signsvfpn  29476  signsvfnn  29477  bnj893  29741  bnj944  29751  bnj969  29759  bnj1136  29808  bnj1177  29817  bnj1452  29863  bnj1489  29867  erdsze2lem1  29928  erdsze2lem2  29929  txsconlem  29965  cvxpcon  29967  cvxscon  29968  cvmsiota  30002  cvmliftiota  30026  cvmlift2lem10  30037  ghomgrp  30310  wsucex  30510  wsuccl  30511  nobndlem2  30581  nofulllem4  30593  altxpsspw  30743  hfuni  30950  tailf  31030  tailfb  31032  bj-snglex  31529  bj-projex  31551  bj-pr1ex  31562  bj-1uplex  31564  bj-pr2ex  31576  bj-2uplex  31578  fin2so  31890  mbfresfi  31945  mbfposadd  31946  cnambfre  31947  itg2addnclem2  31952  ibladdnclem  31956  itgaddnclem1  31958  iblabsnclem  31963  iblmulc2nc  31965  itggt0cn  31972  ftc1cnnclem  31973  ftc1anclem3  31977  ftc1anclem5  31979  ftc1anclem8  31982  ftc1anc  31983  supex2g  32022  sdclem1  32030  constcncf  32049  sub1cncf  32051  sub2cncf  32052  sstotbnd2  32064  equivbnd2  32082  ismtyres  32098  rrnheibor  32127  reheibor  32129  iccbnd  32130  icccmpALT  32131  exidres  32134  exidresid  32135  lshpinN  32518  dalemdea  33190  dalem5  33195  dalem8  33198  dalem9  33200  dalem15  33206  dalem23  33224  cdlemblem  33321  osumcllem1N  33484  osumcllem9N  33492  pexmidlem6N  33503  lhpat2  33573  arglem1N  33719  cdleme0aa  33739  cdleme1b  33755  cdleme1  33756  cdleme2  33757  cdleme3b  33758  cdleme3e  33761  cdleme3h  33764  cdleme7b  33773  cdleme7e  33776  cdleme7ga  33777  cdleme9b  33781  cdleme15d  33806  cdleme22gb  33823  cdlemedb  33826  cdlemeda  33827  cdleme23b  33880  cdleme25cl  33887  cdleme27cl  33896  cdleme29cl  33907  cdlemefs27cl  33943  cdleme42c  34002  cdleme42h  34012  cdleme42i  34013  cdlemg4c  34142  cdlemg4  34147  cdlemg6c  34150  cdlemkvcl  34372  cdlemkoatnle  34381  cdlemk14  34384  cdlemk15  34385  cdlemk29-3  34441  cdlemk37  34444  dia2dimlem1  34595  dvheveccl  34643  diblss  34701  dihglblem5  34829  dih1dimatlem  34860  dihat  34866  dihjatcclem1  34949  dihjatcclem2  34950  dihjatcclem4  34952  dochexmidlem5  34995  dochexmidlem6  34996  lclkrlem2m  35050  lclkrlem2o  35052  lcfrlem3  35075  lcfrlem22  35095  lcfrlem25  35098  lcfrlem30  35103  lcfrlem37  35110  mapdpglem17N  35219  mapdpglem19  35221  hdmap1val  35330  mzpnegmpt  35549  vdioph  35585  3anrabdioph  35588  3orrabdioph  35589  rexrabdioph  35600  rexfrabdioph  35601  2rexfrabdioph  35602  3rexfrabdioph  35603  4rexfrabdioph  35604  6rexfrabdioph  35605  7rexfrabdioph  35606  elnnrabdioph  35613  dvdsrabdioph  35616  eldioph4b  35617  pellfundgt1  35695  jm2.27c  35826  lsmfgcl  35896  lmhmfgima  35906  lmhmlnmsplit  35909  pwssplit4  35911  pwslnm  35916  areaquad  36065  sblpnf  36560  fsumcnf  37247  unidmex  37294  fiiuncl  37313  fiunicl  37315  rnmptfi  37328  suprnmpt  37332  fzisoeu  37404  upbdrech  37409  upbdrech2  37412  fmulcl  37523  ellimciota  37558  constlimc  37568  sumnnodd  37574  addccncf2  37617  cncfiooicclem1  37635  dvresntr  37652  ioodvbdlimc1lem1  37667  ioodvbdlimc1lem2  37668  ioodvbdlimc1lem1OLD  37669  ioodvbdlimc1lem2OLD  37670  ioodvbdlimc2lem  37672  ioodvbdlimc2lemOLD  37673  dvnmul  37682  itgsin0pilem1  37690  itgsinexplem1  37694  mbfres2cn  37699  iblsplit  37707  iblsplitf  37711  stoweidlem2  37726  stoweidlem3  37727  stoweidlem5  37729  stoweidlem16  37740  stoweidlem18  37742  stoweidlem20  37744  stoweidlem21  37745  stoweidlem22  37746  stoweidlem23  37747  stoweidlem31  37756  stoweidlem32  37757  stoweidlem36  37761  stoweidlem40  37765  stoweidlem41  37766  stoweidlem47  37772  stoweidlem50  37775  stoweidlem57  37782  stoweidlem59  37784  stoweidlem60  37785  stoweidlem62  37787  stoweidlem62OLD  37788  wallispi2lem2  37798  dirkertrigeqlem1  37824  dirkeritg  37828  dirkercncflem1  37829  dirkercncflem4  37832  fourierdlem4  37837  fourierdlem6  37839  fourierdlem7  37840  fourierdlem19  37852  fourierdlem20  37853  fourierdlem25  37858  fourierdlem26  37859  fourierdlem30  37863  fourierdlem31  37864  fourierdlem31OLD  37865  fourierdlem32  37866  fourierdlem33  37867  fourierdlem35  37869  fourierdlem36  37870  fourierdlem41  37875  fourierdlem42  37876  fourierdlem42OLD  37877  fourierdlem47  37881  fourierdlem48  37882  fourierdlem49  37883  fourierdlem50  37884  fourierdlem51  37885  fourierdlem52  37886  fourierdlem54  37888  fourierdlem62  37896  fourierdlem63  37897  fourierdlem64  37898  fourierdlem65  37899  fourierdlem71  37905  fourierdlem76  37910  fourierdlem79  37913  fourierdlem80  37914  fourierdlem85  37919  fourierdlem86  37920  fourierdlem87  37921  fourierdlem89  37923  fourierdlem90  37924  fourierdlem91  37925  fourierdlem94  37928  fourierdlem97  37931  fourierdlem102  37936  fourierdlem103  37937  fourierdlem104  37938  fourierdlem107  37941  fourierdlem113  37947  fourierdlem114  37948  fourierswlem  37958  fouriersw  37959  elaa2lem  37961  elaa2lemOLD  37962  etransclem23  37986  etransclem43  38006  etransclem45  38008  etransclem46  38009  etransclem47  38010  etransclem48OLD  38011  etransclem48  38012  sge0split  38083  dmmeasal  38113  caragenunidm  38152  ovnval2  38186  iccpartigtl  38493  3odd  38591  4even  38592  5odd  38593  bgoldbtbndlem2  38657  bgoldbtbndlem3  38658  pfxccatin12lem2  38721  pfxccatin12  38722  pfxccat3  38723  pfxccatpfx2  38725  pfxccat3a  38726  fsummsndifre  38799  fsummmodsndifre  38801  fsummmodsnunz  38802  structiedg0val  38832  snstriedgval  38845  usgrfilem2  39001  usgrafisbaseALT  39094  usgrafisbaseALT2  39095  usgfislem2  39099  usgfisALTlem2  39103  rnghmsscmap2  39317  rhmsscmap2  39363  rhmsscrnghm  39370  fldc  39427  fldhmsubc  39428  fldcALTV  39446  fldhmsubcALTV  39447  mptcfsupp  39509  linply1  39529  lincext1  39591  lincext2  39592  lindslinindimp2lem1  39595  lincresunit1  39614  lincresunit2  39615  fllogbd  39715  dp2cl  39833  aacllem  39884
  Copyright terms: Public domain W3C validator