MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylc Structured version   Visualization version   GIF version

Theorem sylc 65
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1 (𝜑𝜓)
sylc.2 (𝜑𝜒)
sylc.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
sylc (𝜑𝜃)

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3 (𝜑𝜓)
2 sylc.2 . . 3 (𝜑𝜒)
3 sylc.3 . . 3 (𝜓 → (𝜒𝜃))
41, 2, 3syl2im 40 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 52 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl3c  66  mpsyl  68  jc  161  jcnd  163  2thd  265  jca  513  syl2anc  585  unitreslOLD  877  aevlem0  2058  equvel  2456  elex2OLD  3496  elex22  3497  spcedv  3589  rspcdf  3600  rspcdva  3614  rspc3dv  3630  spsbcd  3792  opth  5477  euotd  5514  wereu2  5674  unielrel  6274  frpomin  6342  tz7.7  6391  funmo  6564  funmoOLD  6565  fvelimad  6960  iinpreima  7071  fnfvima  7235  resfvresima  7237  fliftfun  7309  fliftval  7313  weniso  7351  riota5f  7394  riotass2  7396  fovcld  7536  ofmpteq  7692  ssorduni  7766  sucexeloniOLD  7798  suceloniOLD  7800  nlimsucg  7831  tfisi  7848  zfrep6  7941  curry1  8090  curry2  8093  fnwelem  8117  funsssuppss  8175  frrlem4  8274  frrlem8  8278  frrlem10  8280  fprlem1  8285  fprlem2  8286  wfrlem4OLD  8312  smogt  8367  tfrlem5  8380  omeulem1  8582  oeworde  8593  oelimcl  8600  oeeulem  8601  oeeui  8602  nnawordex  8637  oaabs2  8648  naddssim  8684  swoso  8736  qliftlem  8792  resixp  8927  domssl  8994  domssr  8995  undomOLD  9060  xpdom3  9070  domunsncan  9072  omxpenlem  9073  domssex  9138  xpf1o  9139  mapdom3  9149  dif1en  9160  findcard  9163  f1dmvrnfibi  9336  fiin  9417  marypha1lem  9428  marypha1  9429  fisupcl  9464  supgtoreq  9465  ordiso2  9510  ordtypelem2  9514  ordtypelem8  9520  wemapso2lem  9547  unxpwdom2  9583  cantnflt  9667  cantnfrescl  9671  oemapvali  9679  cantnflem1d  9683  wemapwe  9692  cnfcom  9695  ttrclss  9715  ttrclselem2  9721  frrlem15  9752  rankr1id  9857  tcrank  9879  cardmin2  9994  infxpenlem  10008  fseqen  10022  ween  10030  ac5num  10031  indcardi  10036  acni2  10041  fodomfi2  10055  infpwfien  10057  inffien  10058  iunfictbso  10109  acacni  10135  dfac12lem2  10139  djuinf  10183  infmap2  10213  ackbij1lem18  10232  ackbij1b  10234  fictb  10240  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  coftr  10268  infpssrlem4  10301  domfin4  10306  fin2i2  10313  isfin2-2  10314  fincssdom  10318  ssfin3ds  10325  fin23lem20  10332  fin23lem30  10337  isf32lem3  10350  fin1a2lem12  10406  fin1a2lem13  10407  hsmexlem2  10422  axdc2lem  10443  imadomg  10529  fnct  10532  iundom2g  10535  iundomg  10536  iundom  10537  unirnfdomd  10562  konigthlem  10563  iunctb  10569  fpwwe2  10638  canthwelem  10645  pwfseqlem3  10655  pwfseqlem5  10658  winalim2  10691  wunelss  10703  r1wunlim  10732  wunex2  10733  tsksdom  10751  tskinf  10764  inttsk  10769  inar1  10770  tskcard  10776  tskurn  10784  gruina  10813  grur1a  10814  grur1  10815  addsrpr  11070  mulsrpr  11071  lemul12a  12072  lemulge11  12076  lediv12a  12107  fiminre2  12162  nngt0  12243  nn0ge2m1nn  12541  peano5uzi  12651  nn0ind-raph  12662  znnn0nn  12673  suprzub  12923  uzsupss  12924  rpge0  12987  fz0fzelfz0  13607  fz0fzdiffz0  13610  ige2m2fzo  13695  elfzodifsumelfzo  13698  elfzom1elp1fzo  13699  fzonfzoufzol  13735  flltdivnn0lt  13798  fldiv  13825  modaddmodup  13899  uzrdgsuci  13925  fzennn  13933  uzindi  13947  fsuppmapnn0fiubex  13957  expcl2lem  14039  leexp1a  14140  modexp  14201  faclbnd  14250  faclbnd6  14259  facavg  14261  hashginv  14294  hashf1rn  14312  hasheqf1od  14313  seqcoll  14425  hashge2el2dif  14441  wrdsymb0  14499  wrdlenge2n0  14502  ccatsymb  14532  swrdnd2  14605  swrdnd0  14607  pfxnd  14637  pfxccat1  14652  swrdpfx  14657  pfxpfx  14658  wrd2ind  14673  pfxccatin12  14683  pfxccat3  14684  swrdccat  14685  pfxccatpfx1  14686  pfxccatpfx2  14687  swrdccatin1d  14693  pfxccatin12d  14695  repswswrd  14734  cshwidxmod  14753  s2f1o  14867  f1oun2prg  14868  wwlktovfo  14909  relexpfld  14996  rtrclreclem3  15007  resqrex  15197  cau3lem  15301  reusq0  15409  rlimcld2  15522  climcn2  15537  isercoll  15614  climsup  15616  caurcvgr  15620  sumeq2ii  15639  summolem3  15660  zsum  15664  fsumadd  15686  fsumsplit1  15691  fsum2dlem  15716  fsum0diag2  15729  fsummulc2  15730  fsumabs  15747  fsumrelem  15753  fsumrlim  15757  fsumo1  15758  o1fsum  15759  fsumiun  15767  qshash  15773  prodeq2ii  15857  prodmolem3  15877  fprodmul  15904  fproddiv  15905  fprod2dlem  15924  fprodsplit1f  15934  sin02gt0  16135  efieq1re  16142  p1modz1  16204  dvdsleabs2  16255  4dvdseven  16316  sumeven  16330  sumodd  16331  divalglem9  16344  smupvallem  16424  algfx  16517  eucalgcvga  16523  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmflefac  16585  qredeq  16594  fermltl  16717  modprm0  16738  pythagtriplem4  16752  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem12  16759  pythagtriplem13  16760  pythagtriplem14  16761  pythagtriplem16  16763  difsqpwdvds  16820  pcmpt  16825  prmreclem2  16850  4sqlem11  16888  vdwlem9  16922  vdwlem11  16924  vdwlem12  16925  0ram  16953  0ram2  16954  0ramcl  16956  ramcl  16962  prmolelcmf  16981  cshwsidrepsw  17027  cshwshashlem2  17030  prmlem1  17041  prmlem2  17053  strfvd  17134  strfv2d  17135  strssd  17139  firest  17378  prdsdsval3  17431  imasbas  17458  imasds  17459  imasaddfnlem  17474  imasaddvallem  17475  imasvscafn  17483  qusaddvallem  17497  qusaddflem  17498  qusaddval  17499  qusaddf  17500  qusmulval  17501  qusmulf  17502  catideu  17619  idinv  17736  brcici  17747  invfuc  17927  2initoinv  17960  initoeu1w  17962  initoeu2lem0  17963  2termoinv  17967  termoeu1w  17969  mod2ile  18447  lubss  18466  acsmapd  18507  lidrididd  18589  gsumval2a  18604  mndind  18709  submefmnd  18776  mgm2nsgrplem4  18802  qusgrp2  18941  mulgnegnn  18964  pgrpsubgsymg  19277  fvcosymgeq  19297  gsmsymgreqlem1  19298  psgnunilem4  19365  pgpssslw  19482  sylow2alem2  19486  fislw  19493  efgsres  19606  rinvmod  19674  gsumval3lem2  19774  gsumzaddlem  19789  gsum2d  19840  nn0gsumfz  19852  telgsums  19861  dprddomcld  19871  ablfac2  19959  srgdilem  20015  o2timesd  20033  rglcom4d  20034  ringdilem  20072  qusring2  20147  lssintcl  20575  lbsextlem3  20773  lbsextlem4  20774  zringlpirlem3  21034  psgnodpm  21141  psgndiflemB  21153  frlmup4  21356  lindff1  21375  lindfrn  21376  lmisfree  21397  evlseu  21646  mhpmulcl  21692  mptcoe1fsupp  21739  cply1coe0bi  21824  mpfpf1  21870  pf1mpf  21871  mat0dimscm  21971  mdetdiagid  22102  mdet1  22103  mdetunilem9  22122  slesolinv  22182  cramerimp  22188  cpmatmcllem  22220  mptcoe1matfsupp  22304  mp2pm2mp  22313  chpdmat  22343  cctop  22509  subbascn  22758  cnss2  22781  cmpcovf  22895  2ndcctbss  22959  2ndcomap  22962  2ndcsep  22963  comppfsc  23036  ptclsg  23119  dfac14  23122  txcnp  23124  ptcnplem  23125  uptx  23129  txtube  23144  tx2ndc  23155  xkococnlem  23163  elqtop  23201  qtoprest  23221  indishmph  23302  ptcmpfi  23317  kqhmph  23323  csdfil  23398  filssufilg  23415  ufilen  23434  rnelfm  23457  fmfnfmlem4  23461  alexsubALTlem4  23554  ptcmplem4  23559  cnextfvval  23569  cnextcn  23571  cnextfres  23573  tmdgsum2  23600  imasf1oxmet  23881  metss  24017  met2ndci  24031  prdsxmslem2  24038  metust  24067  cfilucfil  24068  metustbl  24075  psmetutop  24076  opnreen  24347  rectbntr0  24348  fsumcn  24386  rescncf  24413  xrhmeo  24462  cnllycmp  24472  lebnumlem1  24477  lebnumlem3  24479  cfilss  24787  iscmet3lem1  24808  iscmet3lem2  24809  ivthicc  24975  ovolsslem  25001  ovoliunlem2  25020  ovoliunnul  25024  ovolicc2lem4  25037  voliunlem3  25069  volsup  25073  uniiccdif  25095  uniioombllem2  25100  volivth  25124  mbfimaopnlem  25172  mbflimsup  25183  i1fd  25198  itg1addlem4  25216  itg1addlem4OLD  25217  itg2addlem  25276  itg2gt0  25278  limciun  25411  dvadd  25457  dvmul  25458  dvco  25464  dvrec  25472  dvcnv  25494  dvferm  25505  rollelem  25506  dvlip  25510  dvlip2  25512  c1liplem1  25513  c1lip2  25515  dvgt0lem1  25519  dvivthlem1  25525  lhop1lem  25530  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcvx  25537  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem4  25546  dvfsumrlim2  25549  dvfsum2  25551  ftc1cn  25560  ftc2ditglem  25562  itgsubstlem  25565  itgpowd  25567  tdeglem4OLD  25578  mdegaddle  25592  mdegmullem  25596  deg1sublt  25628  ply1divmo  25653  fta1g  25685  dgrub  25748  dgrnznn  25761  dgradd2  25782  dvply1  25797  plyrem  25818  aalioulem4  25848  aalioulem5  25849  aalioulem6  25850  aaliou2  25853  taylf  25873  ulmdv  25915  psercn2  25935  abelth  25953  abelth2  25954  reeff1olem  25958  efopn  26166  logreclem  26267  isosctrlem2  26324  xrlimcnp  26473  basellem4  26588  ppiwordi  26666  musum  26695  chpub  26723  gausslemma2dlem0c  26861  2sqlem6  26926  addsqnreup  26946  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  pntlemp  27113  pntleml  27114  ostth3  27141  sltres  27165  noextenddif  27171  nolesgn2ores  27175  nogesgn1ores  27177  nosep1o  27184  nosep2o  27185  nosepeq  27188  nolt02o  27198  noresle  27200  nosupno  27206  nosupbday  27208  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem4  27214  nosupbnd1  27217  nosupbnd2lem1  27218  nosupbnd2  27219  noinfno  27221  noinfbday  27223  noinfres  27225  noinfbnd1lem5  27230  noinfbnd1  27232  noinfbnd2lem1  27233  sltled  27272  madebday  27394  sleadd1  27472  precsexlem10  27662  iscgrglt  27765  colline  27900  axlowdimlem16  28215  axlowdimlem17  28216  axcontlem3  28224  axcontlem10  28231  uhgr2edg  28465  nbupgruvtxres  28664  cusgrres  28705  cusgrfilem2  28713  vdumgr0  28737  frusgrnn0  28828  wlkp1lem8  28937  pthdivtx  28986  upgrwlkdvde  28994  spthonepeq  29009  usgr2pthlem  29020  lfgrn1cycl  29059  wwlknbp1  29098  wwlknllvtx  29100  wlkiswwlks2lem3  29125  umgr2adedgspth  29202  clwlkclwwlklem3  29254  clwwisshclwwslemlem  29266  clwwisshclwws  29268  clwwlkel  29299  wwlksubclwwlk  29311  eleclclwwlknlem1  29313  eleclclwwlknlem2  29314  erclwwlknref  29322  clwwlknonccat  29349  clwwlknonex2lem2  29361  3wlkdlem4  29415  vdn0conngrumgrv2  29449  eucrctshift  29496  frgrnbnb  29546  frgrncvvdeqlem2  29553  frgrncvvdeqlem3  29554  fusgreghash2wspv  29588  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwwlk5  29641  numclwwlk7  29644  frgrreggt1  29646  minvecolem4b  30131  minvecolem4  30133  bcsiALT  30432  ococin  30661  spanpr  30833  pjorthi  30922  nmbdoplbi  31277  nmcoplbi  31281  nmbdfnlbi  31302  nmcfnlbi  31305  nmopcoi  31348  branmfn  31358  hstnmoc  31476  mdsl0  31563  atomli  31635  atcvat4i  31650  atabsi  31654  foresf1o  31742  rabfodom  31743  abrexdomjm  31744  elpreq  31767  ifeqeqx  31774  disjiunel  31827  aciunf1lem  31887  ffsrn  31954  xlt2addrd  31971  supxrnemnf  31981  ssnnssfz  31998  dvdszzq  32021  resspos  32136  resstos  32137  gsummptres2  32205  archirngz  32335  orngsqr  32422  isarchiofld  32435  elrspunidl  32546  drngidlhash  32552  prmidl2  32559  qsidomlem2  32572  ssmxidl  32590  locfinreflem  32820  cmpcref  32830  fmcncfil  32911  xrge0iifiso  32915  elzdif0  32960  qqhval2lem  32961  esumcst  33061  esumrnmpt2  33066  esumpinfval  33071  esumpinfsum  33075  sigaclci  33130  insiga  33135  ldgenpisys  33164  measres  33220  measdivcstALTV  33223  dya2iocnrect  33280  dya2iocnei  33281  omssubadd  33299  carsggect  33317  carsgclctunlem2  33318  sitgclg  33341  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemf  33369  eulerpartlemgh  33377  eulerpartlemgs2  33379  ballotlemfp1  33490  ballotlemfrcn0  33528  ftc2re  33610  fdvposlt  33611  fdvposle  33613  bnj1379  33841  bnj580  33924  bnj944  33949  bnj999  33969  bnj1204  34023  bnj1398  34045  cusgredgex  34112  pthacycspth  34148  derangenlem  34162  subfacp1lem3  34173  resconn  34237  cvmliftlem3  34278  satfv0fvfmla0  34404  satfv1fvfmla1  34414  mrsub0  34507  cgrextend  34980  segconeq  34982  trisegint  35000  fwddifnp1  35137  gg-psercn2  35178  gg-dvfsumle  35182  gg-dvfsumlem2  35183  ivthALT  35220  fnessref  35242  refssfne  35243  neibastop1  35244  filnetlem4  35266  ontgval  35316  unblimceq0lem  35382  unbdqndv2lem2  35386  unbdqndv2  35387  bj-babygodel  35481  bj-alrimd  35497  bj-exlimd  35502  bj-spcimdv  35775  bj-spcimdvv  35776  bj-finsumval0  36166  bj-fvimacnv0  36167  dfgcd3  36205  relowlssretop  36244  relowlpssretop  36245  onsucuni3  36248  finxpreclem4  36275  poimirlem18  36506  poimirlem21  36509  poimirlem25  36513  ftc1cnnclem  36559  ftc1cnnc  36560  ftc2nc  36570  dvasin  36572  dvacos  36573  abrexdom  36598  indexdom  36602  mettrifi  36625  equivtotbnd  36646  totbndbnd  36657  prdstotbnd  36662  heibor1lem  36677  bfplem1  36690  bfplem2  36691  opidonOLD  36720  rngodm1dm2  36800  zerdivemp1x  36815  equid1  37769  omllaw5N  38117  cmtcomlemN  38118  cmtbr3N  38124  omlfh3N  38129  atlen0  38180  exatleN  38275  hlrelat3  38283  cvrexchlem  38290  atlelt  38309  cvrat4  38314  4atlem11b  38479  4atlem12b  38482  lneq2at  38649  cdlema1N  38662  cdlemblem  38664  paddss12  38690  paddasslem2  38692  paddasslem4  38694  paddasslem6  38696  paddasslem12  38702  paddunN  38798  poml4N  38824  poml5N  38825  osumcllem6N  38832  pexmidlem6N  38846  pl42lem2N  38851  ltrnu  38992  ltrneq2  39019  trlval2  39034  cdlemd6  39074  cdleme25b  39225  cdleme29b  39246  cdlemefr29exN  39273  ltrniotacnvval  39453  cdlemk28-3  39779  dochexmidlem7  40337  muldvds2d  40864  fsuppss  41065  frlmsnic  41110  nna4b4nsq  41402  mzpsubmpt  41481  mzpsubst  41486  eqrabdioph  41515  rabdiophlem2  41540  elpell14qr2  41600  elpell1qr2  41610  pellfundre  41619  pellfundge  41620  pellfundglb  41623  pellfund14gap  41625  congabseq  41713  jm2.22  41734  jm2.23  41735  jm2.26lem3  41740  wepwsolem  41784  dnwech  41790  aomclem2  41797  aomclem4  41799  pwfi2f1o  41838  onexlimgt  41992  oaltublim  42040  oege1  42056  cantnfub2  42072  cantnfresb  42074  cantnf2  42075  oacl2g  42080  tfsconcatb0  42094  tfsconcatrev  42098  oaun3lem1  42124  oaun3lem2  42125  nadd2rabtr  42134  nadd1suc  42142  naddsuc2  42143  naddwordnexlem0  42147  naddwordnexlem3  42150  oawordex3  42151  naddwordnexlem4  42152  oaltom  42156  omltoe  42158  ss2iundf  42410  dssmapf1od  42772  neik0pk1imk0  42798  gneispace  42885  grur1cld  42991  cpcolld  43017  mnuop23d  43025  mnuprdlem1  43031  mnuprdlem2  43032  mnurndlem1  43040  grumnudlem  43044  radcnvrat  43073  sbiota1  43193  ordelordALT  43298  2pm13.193  43313  ee11an  43451  refsumcn  43714  rfcnnnub  43720  disjxp1  43756  xrnmnfpnf  43772  ssinc  43776  nssd  43794  disjf1o  43889  disjinfi  43891  choicefi  43899  axccdom  43921  dmrelrnrel  43925  monoords  44007  fperiodmullem  44013  xadd0ge  44030  xrssre  44058  xrlexaddrp  44062  xrred  44075  infxr  44077  xrnpnfmnf  44185  monoordxrv  44192  monoord2xrv  44194  cvgcaule  44202  fsumiunss  44291  fmul01  44296  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1lem1  44300  fmul01lt1lem2  44301  cncfmptss  44303  climinf  44322  climsuselem1  44323  climsuse  44324  limcperiod  44344  limcrecl  44345  sumnnodd  44346  limcleqr  44360  0ellimcdiv  44365  climleltrp  44392  limsuppnfdlem  44417  limsupresxr  44482  liminfresxr  44483  liminfvalxr  44499  cnrefiisplem  44545  xlimmnfvlem1  44548  xlimpnfvlem1  44552  cncfperiod  44595  icccncfext  44603  cncfiooicclem1  44609  dvbdfbdioolem1  44644  dvnmptdivc  44654  dvdsn1add  44655  dvnmptconst  44657  dvnmul  44659  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem2  44663  iblspltprt  44689  itgsubsticclem  44691  itgspltprt  44695  itgsbtaddcnst  44698  stoweidlem3  44719  stoweidlem16  44732  stoweidlem17  44733  stoweidlem19  44735  stoweidlem20  44736  stoweidlem23  44739  stoweidlem25  44741  stoweidlem27  44743  stoweidlem31  44747  stoweidlem34  44750  stoweidlem42  44758  stoweidlem48  44764  stoweidlem51  44767  stoweidlem52  44768  stoweidlem59  44775  wallispilem1  44781  wallispilem3  44783  stirlinglem13  44802  fourierdlem16  44839  fourierdlem20  44843  fourierdlem21  44844  fourierdlem38  44861  fourierdlem42  44865  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem54  44876  fourierdlem68  44890  fourierdlem72  44894  fourierdlem73  44895  fourierdlem76  44898  fourierdlem79  44901  fourierdlem81  44903  fourierdlem86  44908  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem92  44914  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  etransclem24  44974  etransclem25  44975  etransclem28  44978  etransclem41  44991  etransclem44  44994  etransclem48  44998  salexct  45050  dfsalgen2  45057  sge0f1o  45098  sge0rnbnd  45109  sge0split  45125  sge0iunmptlemre  45131  sge0fodjrnlem  45132  sge0iunmpt  45134  nnfoctbdjlem  45171  iundjiunlem  45175  meadjiunlem  45181  ismeannd  45183  meaiuninclem  45196  omeiunle  45233  carageniuncllem1  45237  caratheodorylem1  45242  hoidmvlelem4  45314  hoiqssbllem2  45339  salpreimagelt  45423  salpreimalegt  45425  pimdecfgtioc  45431  smfaddlem2  45480  smflimlem6  45492  nsssmfmbflem  45494  smfpimcclem  45523  or2expropbilem1  45742  funressndmfvrn  45754  f1cof1b  45785  2leaddle2  46006  smonoord  46039  uniimaprimaeqfv  46050  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjALT  46080  iccpartf  46099  ich2exprop  46139  ichnreuop  46140  ichreuopeq  46141  sprbisymrel  46167  fmtnodvds  46212  proththdlem  46281  gbowgt5  46430  gboge9  46432  gbege6  46433  stgoldbwt  46444  sbgoldbalt  46449  bgoldbnnsum3prm  46472  isomgrtrlem  46506  uspgrbisymrelALT  46533  qusrng  46681  ssnn0ssfz  47025  ldepspr  47154  seposep  47558  subthinc  47660  prsthinc  47674  iunord  47721  bnd2d  47726  setrecsss  47746
  Copyright terms: Public domain W3C validator