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  264  jca  512  syl2anc  584  unitreslOLD  876  aevlem0  2057  equvel  2455  elex2OLD  3495  elex22  3496  spcedv  3588  rspcdf  3599  rspcdva  3613  rspc3dv  3629  spsbcd  3791  opth  5476  euotd  5513  wereu2  5673  unielrel  6273  frpomin  6341  tz7.7  6390  funmo  6563  funmoOLD  6564  fvelimad  6959  iinpreima  7070  fnfvima  7234  resfvresima  7236  fliftfun  7308  fliftval  7312  weniso  7350  riota5f  7393  riotass2  7395  fovcld  7535  ofmpteq  7691  ssorduni  7765  sucexeloniOLD  7797  suceloniOLD  7799  nlimsucg  7830  tfisi  7847  zfrep6  7940  curry1  8089  curry2  8092  fnwelem  8116  funsssuppss  8174  frrlem4  8273  frrlem8  8277  frrlem10  8279  fprlem1  8284  fprlem2  8285  wfrlem4OLD  8311  smogt  8366  tfrlem5  8379  omeulem1  8581  oeworde  8592  oelimcl  8599  oeeulem  8600  oeeui  8601  nnawordex  8636  oaabs2  8647  naddssim  8683  swoso  8735  qliftlem  8791  resixp  8926  domssl  8993  domssr  8994  undomOLD  9059  xpdom3  9069  domunsncan  9071  omxpenlem  9072  domssex  9137  xpf1o  9138  mapdom3  9148  dif1en  9159  findcard  9162  f1dmvrnfibi  9335  fiin  9416  marypha1lem  9427  marypha1  9428  fisupcl  9463  supgtoreq  9464  ordiso2  9509  ordtypelem2  9513  ordtypelem8  9519  wemapso2lem  9546  unxpwdom2  9582  cantnflt  9666  cantnfrescl  9670  oemapvali  9678  cantnflem1d  9682  wemapwe  9691  cnfcom  9694  ttrclss  9714  ttrclselem2  9720  frrlem15  9751  rankr1id  9856  tcrank  9878  cardmin2  9993  infxpenlem  10007  fseqen  10021  ween  10029  ac5num  10030  indcardi  10035  acni2  10040  fodomfi2  10054  infpwfien  10056  inffien  10057  iunfictbso  10108  acacni  10134  dfac12lem2  10138  djuinf  10182  infmap2  10212  ackbij1lem18  10231  ackbij1b  10233  fictb  10239  cfslb2n  10262  cofsmo  10263  cfsmolem  10264  coftr  10267  infpssrlem4  10300  domfin4  10305  fin2i2  10312  isfin2-2  10313  fincssdom  10317  ssfin3ds  10324  fin23lem20  10331  fin23lem30  10336  isf32lem3  10349  fin1a2lem12  10405  fin1a2lem13  10406  hsmexlem2  10421  axdc2lem  10442  imadomg  10528  fnct  10531  iundom2g  10534  iundomg  10535  iundom  10536  unirnfdomd  10561  konigthlem  10562  iunctb  10568  fpwwe2  10637  canthwelem  10644  pwfseqlem3  10654  pwfseqlem5  10657  winalim2  10690  wunelss  10702  r1wunlim  10731  wunex2  10732  tsksdom  10750  tskinf  10763  inttsk  10768  inar1  10769  tskcard  10775  tskurn  10783  gruina  10812  grur1a  10813  grur1  10814  addsrpr  11069  mulsrpr  11070  lemul12a  12071  lemulge11  12075  lediv12a  12106  fiminre2  12161  nngt0  12242  nn0ge2m1nn  12540  peano5uzi  12650  nn0ind-raph  12661  znnn0nn  12672  suprzub  12922  uzsupss  12923  rpge0  12986  fz0fzelfz0  13606  fz0fzdiffz0  13609  ige2m2fzo  13694  elfzodifsumelfzo  13697  elfzom1elp1fzo  13698  fzonfzoufzol  13734  flltdivnn0lt  13797  fldiv  13824  modaddmodup  13898  uzrdgsuci  13924  fzennn  13932  uzindi  13946  fsuppmapnn0fiubex  13956  expcl2lem  14038  leexp1a  14139  modexp  14200  faclbnd  14249  faclbnd6  14258  facavg  14260  hashginv  14293  hashf1rn  14311  hasheqf1od  14312  seqcoll  14424  hashge2el2dif  14440  wrdsymb0  14498  wrdlenge2n0  14501  ccatsymb  14531  swrdnd2  14604  swrdnd0  14606  pfxnd  14636  pfxccat1  14651  swrdpfx  14656  pfxpfx  14657  wrd2ind  14672  pfxccatin12  14682  pfxccat3  14683  swrdccat  14684  pfxccatpfx1  14685  pfxccatpfx2  14686  swrdccatin1d  14692  pfxccatin12d  14694  repswswrd  14733  cshwidxmod  14752  s2f1o  14866  f1oun2prg  14867  wwlktovfo  14908  relexpfld  14995  rtrclreclem3  15006  resqrex  15196  cau3lem  15300  reusq0  15408  rlimcld2  15521  climcn2  15536  isercoll  15613  climsup  15615  caurcvgr  15619  sumeq2ii  15638  summolem3  15659  zsum  15663  fsumadd  15685  fsumsplit1  15690  fsum2dlem  15715  fsum0diag2  15728  fsummulc2  15729  fsumabs  15746  fsumrelem  15752  fsumrlim  15756  fsumo1  15757  o1fsum  15758  fsumiun  15766  qshash  15772  prodeq2ii  15856  prodmolem3  15876  fprodmul  15903  fproddiv  15904  fprod2dlem  15923  fprodsplit1f  15933  sin02gt0  16134  efieq1re  16141  p1modz1  16203  dvdsleabs2  16254  4dvdseven  16315  sumeven  16329  sumodd  16330  divalglem9  16343  smupvallem  16423  algfx  16516  eucalgcvga  16522  lcmfunsnlem1  16573  lcmfunsnlem2lem1  16574  lcmflefac  16584  qredeq  16593  fermltl  16716  modprm0  16737  pythagtriplem4  16751  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem12  16758  pythagtriplem13  16759  pythagtriplem14  16760  pythagtriplem16  16762  difsqpwdvds  16819  pcmpt  16824  prmreclem2  16849  4sqlem11  16887  vdwlem9  16921  vdwlem11  16923  vdwlem12  16924  0ram  16952  0ram2  16953  0ramcl  16955  ramcl  16961  prmolelcmf  16980  cshwsidrepsw  17026  cshwshashlem2  17029  prmlem1  17040  prmlem2  17052  strfvd  17133  strfv2d  17134  strssd  17138  firest  17377  prdsdsval3  17430  imasbas  17457  imasds  17458  imasaddfnlem  17473  imasaddvallem  17474  imasvscafn  17482  qusaddvallem  17496  qusaddflem  17497  qusaddval  17498  qusaddf  17499  qusmulval  17500  qusmulf  17501  catideu  17618  idinv  17735  brcici  17746  invfuc  17926  2initoinv  17959  initoeu1w  17961  initoeu2lem0  17962  2termoinv  17966  termoeu1w  17968  mod2ile  18446  lubss  18465  acsmapd  18506  lidrididd  18588  gsumval2a  18603  mndind  18708  submefmnd  18775  mgm2nsgrplem4  18801  qusgrp2  18940  mulgnegnn  18963  pgrpsubgsymg  19276  fvcosymgeq  19296  gsmsymgreqlem1  19297  psgnunilem4  19364  pgpssslw  19481  sylow2alem2  19485  fislw  19492  efgsres  19605  rinvmod  19673  gsumval3lem2  19773  gsumzaddlem  19788  gsum2d  19839  nn0gsumfz  19851  telgsums  19860  dprddomcld  19870  ablfac2  19958  srgdilem  20014  o2timesd  20032  rglcom4d  20033  ringdilem  20071  qusring2  20146  lssintcl  20574  lbsextlem3  20772  lbsextlem4  20773  zringlpirlem3  21033  psgnodpm  21140  psgndiflemB  21152  frlmup4  21355  lindff1  21374  lindfrn  21375  lmisfree  21396  evlseu  21645  mhpmulcl  21691  mptcoe1fsupp  21738  cply1coe0bi  21823  mpfpf1  21869  pf1mpf  21870  mat0dimscm  21970  mdetdiagid  22101  mdet1  22102  mdetunilem9  22121  slesolinv  22181  cramerimp  22187  cpmatmcllem  22219  mptcoe1matfsupp  22303  mp2pm2mp  22312  chpdmat  22342  cctop  22508  subbascn  22757  cnss2  22780  cmpcovf  22894  2ndcctbss  22958  2ndcomap  22961  2ndcsep  22962  comppfsc  23035  ptclsg  23118  dfac14  23121  txcnp  23123  ptcnplem  23124  uptx  23128  txtube  23143  tx2ndc  23154  xkococnlem  23162  elqtop  23200  qtoprest  23220  indishmph  23301  ptcmpfi  23316  kqhmph  23322  csdfil  23397  filssufilg  23414  ufilen  23433  rnelfm  23456  fmfnfmlem4  23460  alexsubALTlem4  23553  ptcmplem4  23558  cnextfvval  23568  cnextcn  23570  cnextfres  23572  tmdgsum2  23599  imasf1oxmet  23880  metss  24016  met2ndci  24030  prdsxmslem2  24037  metust  24066  cfilucfil  24067  metustbl  24074  psmetutop  24075  opnreen  24346  rectbntr0  24347  fsumcn  24385  rescncf  24412  xrhmeo  24461  cnllycmp  24471  lebnumlem1  24476  lebnumlem3  24478  cfilss  24786  iscmet3lem1  24807  iscmet3lem2  24808  ivthicc  24974  ovolsslem  25000  ovoliunlem2  25019  ovoliunnul  25023  ovolicc2lem4  25036  voliunlem3  25068  volsup  25072  uniiccdif  25094  uniioombllem2  25099  volivth  25123  mbfimaopnlem  25171  mbflimsup  25182  i1fd  25197  itg1addlem4  25215  itg1addlem4OLD  25216  itg2addlem  25275  itg2gt0  25277  limciun  25410  dvadd  25456  dvmul  25457  dvco  25463  dvrec  25471  dvcnv  25493  dvferm  25504  rollelem  25505  dvlip  25509  dvlip2  25511  c1liplem1  25512  c1lip2  25514  dvgt0lem1  25518  dvivthlem1  25524  lhop1lem  25529  dvcnvrelem1  25533  dvcnvrelem2  25534  dvcvx  25536  dvfsumle  25537  dvfsumabs  25539  dvfsumlem1  25542  dvfsumlem2  25543  dvfsumlem4  25545  dvfsumrlim2  25548  dvfsum2  25550  ftc1cn  25559  ftc2ditglem  25561  itgsubstlem  25564  itgpowd  25566  tdeglem4OLD  25577  mdegaddle  25591  mdegmullem  25595  deg1sublt  25627  ply1divmo  25652  fta1g  25684  dgrub  25747  dgrnznn  25760  dgradd2  25781  dvply1  25796  plyrem  25817  aalioulem4  25847  aalioulem5  25848  aalioulem6  25849  aaliou2  25852  taylf  25872  ulmdv  25914  psercn2  25934  abelth  25952  abelth2  25953  reeff1olem  25957  efopn  26165  logreclem  26264  isosctrlem2  26321  xrlimcnp  26470  basellem4  26585  ppiwordi  26663  musum  26692  chpub  26720  gausslemma2dlem0c  26858  2sqlem6  26923  addsqnreup  26943  2sqreulem1  26946  2sqreunnlem1  26949  dchrisumlema  26988  dchrisumlem2  26990  dchrisumlem3  26991  pntlemp  27110  pntleml  27111  ostth3  27138  sltres  27162  noextenddif  27168  nolesgn2ores  27172  nogesgn1ores  27174  nosep1o  27181  nosep2o  27182  nosepeq  27185  nolt02o  27195  noresle  27197  nosupno  27203  nosupbday  27205  nosupres  27207  nosupbnd1lem1  27208  nosupbnd1lem4  27211  nosupbnd1  27214  nosupbnd2lem1  27215  nosupbnd2  27216  noinfno  27218  noinfbday  27220  noinfres  27222  noinfbnd1lem5  27227  noinfbnd1  27229  noinfbnd2lem1  27230  sltled  27269  madebday  27391  sleadd1  27469  precsexlem10  27659  iscgrglt  27762  colline  27897  axlowdimlem16  28212  axlowdimlem17  28213  axcontlem3  28221  axcontlem10  28228  uhgr2edg  28462  nbupgruvtxres  28661  cusgrres  28702  cusgrfilem2  28710  vdumgr0  28734  frusgrnn0  28825  wlkp1lem8  28934  pthdivtx  28983  upgrwlkdvde  28991  spthonepeq  29006  usgr2pthlem  29017  lfgrn1cycl  29056  wwlknbp1  29095  wwlknllvtx  29097  wlkiswwlks2lem3  29122  umgr2adedgspth  29199  clwlkclwwlklem3  29251  clwwisshclwwslemlem  29263  clwwisshclwws  29265  clwwlkel  29296  wwlksubclwwlk  29308  eleclclwwlknlem1  29310  eleclclwwlknlem2  29311  erclwwlknref  29319  clwwlknonccat  29346  clwwlknonex2lem2  29358  3wlkdlem4  29412  vdn0conngrumgrv2  29446  eucrctshift  29493  frgrnbnb  29543  frgrncvvdeqlem2  29550  frgrncvvdeqlem3  29551  fusgreghash2wspv  29585  numclwwlk2lem1  29626  numclwlk2lem2f  29627  numclwwlk5  29638  numclwwlk7  29641  frgrreggt1  29643  minvecolem4b  30126  minvecolem4  30128  bcsiALT  30427  ococin  30656  spanpr  30828  pjorthi  30917  nmbdoplbi  31272  nmcoplbi  31276  nmbdfnlbi  31297  nmcfnlbi  31300  nmopcoi  31343  branmfn  31353  hstnmoc  31471  mdsl0  31558  atomli  31630  atcvat4i  31645  atabsi  31649  foresf1o  31737  rabfodom  31738  abrexdomjm  31739  elpreq  31762  ifeqeqx  31769  disjiunel  31822  aciunf1lem  31882  ffsrn  31949  xlt2addrd  31966  supxrnemnf  31976  ssnnssfz  31993  dvdszzq  32016  resspos  32131  resstos  32132  gsummptres2  32200  archirngz  32330  orngsqr  32417  isarchiofld  32430  elrspunidl  32541  drngidlhash  32547  prmidl2  32554  qsidomlem2  32567  ssmxidl  32585  locfinreflem  32815  cmpcref  32825  fmcncfil  32906  xrge0iifiso  32910  elzdif0  32955  qqhval2lem  32956  esumcst  33056  esumrnmpt2  33061  esumpinfval  33066  esumpinfsum  33070  sigaclci  33125  insiga  33130  ldgenpisys  33159  measres  33215  measdivcstALTV  33218  dya2iocnrect  33275  dya2iocnei  33276  omssubadd  33294  carsggect  33312  carsgclctunlem2  33313  sitgclg  33336  eulerpartlemsv2  33352  eulerpartlemv  33358  eulerpartlemf  33364  eulerpartlemgh  33372  eulerpartlemgs2  33374  ballotlemfp1  33485  ballotlemfrcn0  33523  ftc2re  33605  fdvposlt  33606  fdvposle  33608  bnj1379  33836  bnj580  33919  bnj944  33944  bnj999  33964  bnj1204  34018  bnj1398  34040  cusgredgex  34107  pthacycspth  34143  derangenlem  34157  subfacp1lem3  34168  resconn  34232  cvmliftlem3  34273  satfv0fvfmla0  34399  satfv1fvfmla1  34409  mrsub0  34502  cgrextend  34975  segconeq  34977  trisegint  34995  fwddifnp1  35132  gg-psercn2  35173  gg-dvfsumle  35177  gg-dvfsumlem2  35178  ivthALT  35215  fnessref  35237  refssfne  35238  neibastop1  35239  filnetlem4  35261  ontgval  35311  unblimceq0lem  35377  unbdqndv2lem2  35381  unbdqndv2  35382  bj-babygodel  35476  bj-alrimd  35492  bj-exlimd  35497  bj-spcimdv  35770  bj-spcimdvv  35771  bj-finsumval0  36161  bj-fvimacnv0  36162  dfgcd3  36200  relowlssretop  36239  relowlpssretop  36240  onsucuni3  36243  finxpreclem4  36270  poimirlem18  36501  poimirlem21  36504  poimirlem25  36508  ftc1cnnclem  36554  ftc1cnnc  36555  ftc2nc  36565  dvasin  36567  dvacos  36568  abrexdom  36593  indexdom  36597  mettrifi  36620  equivtotbnd  36641  totbndbnd  36652  prdstotbnd  36657  heibor1lem  36672  bfplem1  36685  bfplem2  36686  opidonOLD  36715  rngodm1dm2  36795  zerdivemp1x  36810  equid1  37764  omllaw5N  38112  cmtcomlemN  38113  cmtbr3N  38119  omlfh3N  38124  atlen0  38175  exatleN  38270  hlrelat3  38278  cvrexchlem  38285  atlelt  38304  cvrat4  38309  4atlem11b  38474  4atlem12b  38477  lneq2at  38644  cdlema1N  38657  cdlemblem  38659  paddss12  38685  paddasslem2  38687  paddasslem4  38689  paddasslem6  38691  paddasslem12  38697  paddunN  38793  poml4N  38819  poml5N  38820  osumcllem6N  38827  pexmidlem6N  38841  pl42lem2N  38846  ltrnu  38987  ltrneq2  39014  trlval2  39029  cdlemd6  39069  cdleme25b  39220  cdleme29b  39241  cdlemefr29exN  39268  ltrniotacnvval  39448  cdlemk28-3  39774  dochexmidlem7  40332  muldvds2d  40859  fsuppss  41067  frlmsnic  41112  nna4b4nsq  41403  mzpsubmpt  41471  mzpsubst  41476  eqrabdioph  41505  rabdiophlem2  41530  elpell14qr2  41590  elpell1qr2  41600  pellfundre  41609  pellfundge  41610  pellfundglb  41613  pellfund14gap  41615  congabseq  41703  jm2.22  41724  jm2.23  41725  jm2.26lem3  41730  wepwsolem  41774  dnwech  41780  aomclem2  41787  aomclem4  41789  pwfi2f1o  41828  onexlimgt  41982  oaltublim  42030  oege1  42046  cantnfub2  42062  cantnfresb  42064  cantnf2  42065  oacl2g  42070  tfsconcatb0  42084  tfsconcatrev  42088  oaun3lem1  42114  oaun3lem2  42115  nadd2rabtr  42124  nadd1suc  42132  naddsuc2  42133  naddwordnexlem0  42137  naddwordnexlem3  42140  oawordex3  42141  naddwordnexlem4  42142  oaltom  42146  omltoe  42148  ss2iundf  42400  dssmapf1od  42762  neik0pk1imk0  42788  gneispace  42875  grur1cld  42981  cpcolld  43007  mnuop23d  43015  mnuprdlem1  43021  mnuprdlem2  43022  mnurndlem1  43030  grumnudlem  43034  radcnvrat  43063  sbiota1  43183  ordelordALT  43288  2pm13.193  43303  ee11an  43441  refsumcn  43704  rfcnnnub  43710  disjxp1  43746  xrnmnfpnf  43762  ssinc  43766  nssd  43784  disjf1o  43879  disjinfi  43881  choicefi  43889  axccdom  43911  dmrelrnrel  43915  monoords  43997  fperiodmullem  44003  xadd0ge  44020  xrssre  44048  xrlexaddrp  44052  xrred  44065  infxr  44067  xrnpnfmnf  44175  monoordxrv  44182  monoord2xrv  44184  cvgcaule  44192  fsumiunss  44281  fmul01  44286  fmuldfeqlem1  44288  fmuldfeq  44289  fmul01lt1lem1  44290  fmul01lt1lem2  44291  cncfmptss  44293  climinf  44312  climsuselem1  44313  climsuse  44314  limcperiod  44334  limcrecl  44335  sumnnodd  44336  limcleqr  44350  0ellimcdiv  44355  climleltrp  44382  limsuppnfdlem  44407  limsupresxr  44472  liminfresxr  44473  liminfvalxr  44489  cnrefiisplem  44535  xlimmnfvlem1  44538  xlimpnfvlem1  44542  cncfperiod  44585  icccncfext  44593  cncfiooicclem1  44599  dvbdfbdioolem1  44634  dvnmptdivc  44644  dvdsn1add  44645  dvnmptconst  44647  dvnmul  44649  dvmptfprodlem  44650  dvmptfprod  44651  dvnprodlem2  44653  iblspltprt  44679  itgsubsticclem  44681  itgspltprt  44685  itgsbtaddcnst  44688  stoweidlem3  44709  stoweidlem16  44722  stoweidlem17  44723  stoweidlem19  44725  stoweidlem20  44726  stoweidlem23  44729  stoweidlem25  44731  stoweidlem27  44733  stoweidlem31  44737  stoweidlem34  44740  stoweidlem42  44748  stoweidlem48  44754  stoweidlem51  44757  stoweidlem52  44758  stoweidlem59  44765  wallispilem1  44771  wallispilem3  44773  stirlinglem13  44792  fourierdlem16  44829  fourierdlem20  44833  fourierdlem21  44834  fourierdlem38  44851  fourierdlem42  44855  fourierdlem46  44858  fourierdlem48  44860  fourierdlem49  44861  fourierdlem50  44862  fourierdlem54  44866  fourierdlem68  44880  fourierdlem72  44884  fourierdlem73  44885  fourierdlem76  44888  fourierdlem79  44891  fourierdlem81  44893  fourierdlem86  44898  fourierdlem89  44901  fourierdlem90  44902  fourierdlem91  44903  fourierdlem92  44904  fourierdlem97  44909  fourierdlem101  44913  fourierdlem103  44915  fourierdlem104  44916  fourierdlem111  44923  etransclem24  44964  etransclem25  44965  etransclem28  44968  etransclem41  44981  etransclem44  44984  etransclem48  44988  salexct  45040  dfsalgen2  45047  sge0f1o  45088  sge0rnbnd  45099  sge0split  45115  sge0iunmptlemre  45121  sge0fodjrnlem  45122  sge0iunmpt  45124  nnfoctbdjlem  45161  iundjiunlem  45165  meadjiunlem  45171  ismeannd  45173  meaiuninclem  45186  omeiunle  45223  carageniuncllem1  45227  caratheodorylem1  45232  hoidmvlelem4  45304  hoiqssbllem2  45329  salpreimagelt  45413  salpreimalegt  45415  pimdecfgtioc  45421  smfaddlem2  45470  smflimlem6  45482  nsssmfmbflem  45484  smfpimcclem  45513  or2expropbilem1  45732  funressndmfvrn  45744  f1cof1b  45775  2leaddle2  45996  smonoord  46029  uniimaprimaeqfv  46040  fundcmpsurbijinjpreimafv  46065  fundcmpsurinjALT  46070  iccpartf  46089  ich2exprop  46129  ichnreuop  46130  ichreuopeq  46131  sprbisymrel  46157  fmtnodvds  46202  proththdlem  46271  gbowgt5  46420  gboge9  46422  gbege6  46423  stgoldbwt  46434  sbgoldbalt  46439  bgoldbnnsum3prm  46462  isomgrtrlem  46496  uspgrbisymrelALT  46523  qusrng  46671  ssnn0ssfz  47015  ldepspr  47144  seposep  47548  subthinc  47650  prsthinc  47664  iunord  47711  bnd2d  47716  setrecsss  47736
  Copyright terms: Public domain W3C validator