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

Theorem simpll 746
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )

Proof of Theorem simpll
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
21ad2antrr 718 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  simp1ll  1044  simp2ll  1048  simp3ll  1052  pm2.61da3ne  2681  rmob  3274  ifboth  3813  prneimg  4041  ordelord  4728  poinxp  4889  soltmin  5225  xpdifid  5254  sofld  5274  f1oprswap  5668  mpteqb  5776  fvmptt  5777  iinpreima  5821  nvocnv  5975  fcof1  5978  soisoi  6006  grprinvlem  6290  fnfvof  6322  fvn0elsupp  6695  suppssov1  6710  suppssfv  6714  dftpos4  6753  tfrlem3a  6822  tfrlem9a  6831  oaass  6988  oelimcl  7027  nnawordex  7064  oaabs  7071  oaabs2  7072  omabs  7074  qsel  7167  th3qlem1  7194  mapss  7243  boxcutc  7294  omxpenlem  7400  xpmapenlem  7466  mapdom2  7470  unxpdomlem3  7507  f1finf1o  7527  frfi  7545  nnunifi  7551  indexfi  7607  fsuppsssupp  7624  elfi2  7652  elfiun  7668  marypha1lem  7671  supisolem  7708  ordtypelem7  7726  oismo  7742  wdomtr  7778  brwdom3  7785  cnfcomlem  7920  cnfcomlemOLD  7928  r1ordg  7973  rankval3b  8021  rankonidlem  8023  harcard  8136  infxpenlem  8168  acni2  8204  numacn  8207  fodomacn  8214  mappwen  8270  dfac9  8293  cdalepw  8353  infxpabs  8369  infunsdom1  8370  infunsdom  8371  ackbij1lem15  8391  cfsmolem  8427  infpssrlem5  8464  infpssr  8465  ssfin4  8467  fin2i2  8475  ssfin2  8477  fin23lem24  8479  fin23lem22  8484  fin23lem27  8485  fin23lem36  8505  isf32lem3  8512  isf32lem7  8516  isf34lem7  8536  fin1a2lem13  8569  hsmexlem4  8586  axdc4lem  8612  iundom2g  8692  alephexp1  8731  fpwwe2lem1  8786  fpwwe2lem8  8792  canthp1  8809  inttsk  8929  inar1  8930  r1tskina  8937  grur1  8975  nqerf  9087  distrlem1pr  9182  distrlem4pr  9183  reclem2pr  9205  addsub4  9640  le2add  9809  lt2sub  9825  le2sub  9826  mulge0  9845  receu  9969  rec11  10017  rec11r  10018  divdivdiv  10020  ddcan  10033  divadddiv  10034  divsubdiv  10035  conjmul  10036  rereccl  10037  subrec  10148  recgt0  10161  prodgt0  10162  prodge0  10164  ltmul12a  10173  lemul12a  10175  lemulge11  10179  mulge0b  10187  lt2mul2div  10196  ltrec  10201  lerec  10202  lt2msq  10204  le2msq  10220  msq11  10221  ledivp1  10222  rimul  10301  uzletr  10857  zsupss  10932  uzwo3  10936  qreccl  10961  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem5  10971  qbtwnre  11157  qbtwnxr  11158  xralrple  11163  xpncan  11202  xaddge0  11209  xle2add  11210  xmulneg1  11220  xmulgt0  11234  ixxss1  11306  ixxss2  11307  elioc2  11346  difreicc  11404  divelunit  11414  fzass4  11483  fzrev  11503  fzonmapblen  11576  fzocatel  11586  elfzodifsumelfzo  11588  ssfzo12bi  11606  modid  11716  uzindi  11787  seqfeq3  11840  seqof2  11848  expcl2lem  11861  expnegz  11882  expadd  11890  expmul  11893  expcan  11900  ltexp2  11901  leexp1a  11906  expnlbnd  11978  digit1  11982  bcval5  12078  bcpasc  12081  hashprb  12141  fzsdom2  12173  hashimarn  12184  hashbclem  12189  hashbc  12190  hashf1lem2  12193  seqcoll  12200  swrdn0  12308  swrdvalodm2  12317  swrdsymbeq  12325  wrdeqswrdlsw  12327  ccatswrd  12334  wrd2ind  12356  swrdccatin12lem2  12364  swrdccatin12lem3  12365  swrdccatin12  12366  swrdccat3  12367  revccat  12390  reps  12392  repswrevw  12408  sqrmul  12733  sqrlt  12735  sqrdiv  12739  absexpz  12778  abslt  12786  absle  12787  abssubne0  12788  rexico  12825  amgm2  12841  rlim3  12960  lo1bdd2  12986  climuni  13014  rlimcn1  13050  cn1lem  13059  iserex  13118  iserle  13121  isercolllem1  13126  climcau  13132  caucvgb  13141  iseralt  13146  summo  13178  zsum  13179  sumss2  13187  isumadd  13218  fsum2dlem  13221  fsum2d  13222  fsum0diag2  13233  fsumabs  13247  cvgcmp  13262  cvgcmpce  13264  incexclem  13282  incexc2  13284  isumsplit  13286  climcnds  13297  divrcnv  13298  geolim  13313  geo2lim  13318  geomulcvg  13319  mertenslem1  13327  mertenslem2  13328  mertens  13329  efcvgfsum  13354  eftlcl  13374  reeftlcl  13375  tanadd  13434  eirr  13470  rpnnen2  13491  sqr2irr  13514  dvds2ln  13546  dvdseq  13563  dvdsext  13567  bitsfzo  13614  sadadd2lem2  13629  sadadd  13646  bitsshft  13654  smupvallem  13662  smumul  13672  bezout  13709  gcdmultiplez  13718  dvdsmulgcd  13721  prmdvdsexp  13783  pcqmul  13903  pcexp  13909  pcneg  13923  pcdvdstr  13925  pcprmpw2  13931  pcfac  13944  expnprm  13947  prmpwdvds  13948  prmreclem6  13965  mul4sq  13998  vdwapf  14016  vdwlem13  14037  vdw  14038  vdwnnlem3  14041  vdwnn  14042  ramub2  14058  ramz  14069  ramcl  14073  cshwsidrepswmod0  14104  cshwshashlem1  14105  ressress  14218  pwsle  14413  mreriincl  14519  mrcuni  14542  mreexexlemd  14565  isacs2  14574  acsfn  14580  acsfn1  14582  acsfn2  14584  iscat  14593  cidfval  14597  iscatd2  14602  monfval  14654  isfunc  14757  isfull2  14804  isfth2  14808  1stfval  14984  2ndfval  14987  yonedainv  15074  drsdirfi  15091  pospo  15126  lejoin1  15165  lemeet1  15179  mod1ile  15258  mod2ile  15259  isipodrs  15314  isacs4lem  15321  mrelatlub  15339  submnd0  15434  resmhm  15469  mhmco  15472  mhmima  15473  pwsdiagmhm  15479  gsumwsubmcl  15496  gsumwmhm  15503  gsumwspan  15504  grprcan  15551  grplactcnv  15604  mulgz  15628  mulgnn0dir  15630  mulgdir  15632  mulgneg2  15634  mulgnn0ass  15636  mhmmulg  15639  pwssub  15648  pwsmulg  15649  issubg4  15680  nmzsubg  15702  ssnmz  15703  ghmmhmb  15738  resghm  15743  ghmpreima  15748  ghmnsgpreima  15751  ghmf1o  15756  isga  15789  gaid  15797  gass  15799  gapm  15804  gaorber  15806  gastacl  15807  gastacos  15808  cntzsubm  15833  cntzsubg  15834  cntzmhm  15836  lactghmga  15889  f1omvdconj  15932  pmtrfinv  15947  symggen  15956  psgnunilem3  15982  submod  16048  gexdvds  16063  gexcl3  16066  sylow2blem3  16101  lsmub1x  16125  lsmless12  16140  pj1id  16176  efglem  16193  efgcpbllemb  16232  mulgnn0di  16293  eqgabl  16299  gexex  16315  torsubg  16316  cygabl  16347  prmcyg  16350  cyggexb  16355  gsumval3OLD  16362  gsumval3  16365  subgdmdprd  16505  mgpress  16576  isrng  16585  rngpropd  16612  dvdsrtr  16678  isdrng2  16766  issubrg  16789  cntzsubr  16821  abvrec  16845  abvdiv  16846  islmodd  16878  lmodprop2d  16931  lssvsubcl  16947  lssvacl  16957  lssvscl  16958  islss3  16962  lss1d  16966  lsspropd  17020  islmhm  17030  lmhmco  17046  lmhmplusg  17047  lmhmf1o  17049  lmhmima  17050  lmhmpreima  17051  reslmhm  17055  lspextmo  17059  pwsdiaglmhm  17060  lmhmpropd  17076  islbs2  17157  lidlsubcl  17220  drngnidl  17233  2idlcpbl  17238  unitrrg  17287  fidomndrng  17301  issubassa  17317  assapropd  17320  psrbaglefi  17375  psrbaglefiOLD  17376  psrbagconf1o  17378  coe1mul2lem1  17619  ply1coe  17643  qsssubdrg  17716  cnsubrg  17717  zringlpir  17748  zlpir  17753  domnchr  17805  znval  17808  znunit  17838  znrrg  17840  evpmodpmf1o  17868  psgndif  17874  isphl  17899  ocvlss  17939  ocvin  17941  obslbs  17997  dsmmbas2  18004  dsmmfi  18005  frlmipval  18046  frlmlbs  18067  lindfind  18087  lindfrn  18092  islindf3  18097  grpvrinv  18138  matrng  18172  matassa  18173  mat1  18176  ma1repvcl  18223  mdetunilem8  18267  madutpos  18290  symgmatr01lem  18301  gsummatr01lem4  18306  smadiadet  18318  matunit  18326  toponmre  18539  neissex  18573  clslp  18594  tgrest  18605  restcld  18618  ssrest  18622  restopn2  18623  pnfnei  18666  mnfnei  18667  cnpnei  18710  cnco  18712  cnss1  18722  cnss2  18723  isnrm2  18804  restcnrm  18808  dnsconst  18824  cmpsub  18845  uncmp  18848  dfcon2  18865  2ndcrest  18900  1stcelcls  18907  hausllycmp  18940  cldllycmp  18941  dislly  18943  kgencn  18971  ptpjpre2  18995  ptclsg  19030  dfac14  19033  txindis  19049  txlly  19051  txnlly  19052  txcmp  19058  xkoptsub  19069  xkopt  19070  xkoinjcn  19102  qtopkgen  19125  kqdisj  19147  kqcldsat  19148  isr0  19152  kqreglem2  19157  kqnrmlem2  19159  nrmr0reg  19164  reghmph  19208  nrmhmph  19209  infil  19278  fgabs  19294  filcon  19298  trfil2  19302  isufil2  19323  trufil  19325  filssufilg  19326  ssufl  19333  ufileu  19334  rnelfm  19368  fbflim  19391  flimclsi  19393  flimsncls  19401  hauspwpwf1  19402  fclsval  19423  fclscf  19440  flimfnfcls  19443  uffclsflim  19446  alexsubb  19460  cnextcn  19481  tmdmulg  19505  symgtgp  19514  utoptop  19651  utopsnneiplem  19664  psmetres2  19732  xmetres2  19778  xblss2ps  19818  blhalf  19822  blssexps  19843  blssex  19844  blin2  19846  blbas  19847  met1stc  19938  met2ndci  19939  metcnpi  19961  metcnpi2  19962  metusttoOLD  19974  metustto  19975  metustexhalfOLD  19980  metustexhalf  19981  elbl4  19993  metuel2  19996  dscopn  20008  ngpinvds  20046  subgngp  20063  tngngp  20082  nmdvr  20093  nlmvscn  20110  nrginvrcn  20114  lssnlm  20123  nmoco  20158  blcvx  20217  tgqioo  20219  icccmplem2  20242  metdstri  20269  metdsle  20270  metdsre  20271  cncfss  20317  icoopnst  20353  phtpycc  20405  phtpc01  20410  pcohtpylem  20433  clmmulg  20507  iscph  20531  ipcn  20600  csscld  20603  clsocv  20604  cfilfcls  20627  cmetcau  20642  iscmet3lem2  20645  lmclim  20655  flimcfil  20666  cmetss  20667  bcth  20682  bcth2  20683  cmetcuspOLD  20707  cmetcusp  20708  ivthicc  20784  ovolficc  20794  ovolctb  20815  ovolun  20824  ovolfiniun  20826  ovoliunlem2  20828  ovoliunlem3  20829  ovolicc2lem3  20844  ovolicc2lem4  20845  unmbl  20861  shftmbl  20862  volfiniun  20870  voliunlem3  20875  volsup  20879  ioombl  20888  volcn  20928  volivth  20929  vitalilem1  20930  mbfconstlem  20949  mbfposr  20972  cnmbf  20979  mbflimsup  20986  i1fd  21001  i1f1  21010  itg10a  21030  itg2le  21059  itg2const2  21061  iblss  21124  itgeqa  21133  bddmulibl  21158  cnplimc  21204  limccnp2  21209  dvres  21228  dvnres  21247  dvcj  21266  dvrec  21271  dvmptfsum  21289  dvexp3  21292  dveflem  21293  dvfsumrlimge0  21344  evlsval  21371  tdeglem4  21414  ply1domn  21480  elply2  21549  ply1termlem  21556  plypf1  21565  plymullem1  21567  dgrlem  21582  coeid  21591  coeeq2  21595  coemulc  21607  dgreq0  21617  dvply2g  21636  plydivalg  21650  plyexmo  21664  elqaa  21673  aaliou3lem8  21696  dvtaylp  21720  mtest  21754  abelthlem2  21782  ptolemy  21843  cosord  21873  logdivle  21956  divlogrlim  21965  logcnlem5  21976  logtayl  21990  cxpmul2  22019  abscxp2  22023  cxplt  22024  cxple  22025  cxplt3  22030  atantayl3  22219  birthdaylem3  22232  rlimcnp2  22245  efrlim  22248  cxploglim2  22257  scvxcvx  22264  fta  22302  efnnfsumcl  22325  isppw2  22338  sqf11  22362  sgmval  22365  sgmval2  22366  efchtdvds  22382  sqff1o  22405  sgmmul  22425  pclogsum  22439  vmasum  22440  logfac2  22441  logexprlim  22449  perfect  22455  dchrelbas4  22467  dchrptlem2  22489  bcmax  22502  bposlem1  22508  bpos  22517  lgslem4  22523  lgsdir2lem5  22551  2sqlem6  22593  dchrisumlem3  22625  dchrmusum2  22628  pntrlog2bnd  22718  pntlem3  22743  pnt3  22746  qabvexp  22760  ostth  22773  axtgcont  22815  iscgrg  22846  tgisline  22906  colline  22918  mirval  22925  ttgbtwnid  22953  colinearalglem4  22978  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  axcontlem8  23040  axcontlem9  23041  axcontlem10  23042  elntg  23053  eengtrkg  23054  umgra1  23083  uslgra1  23114  usgra1  23115  usgraedg4  23128  wlkres  23251  wlkbprop  23256  0pthon  23301  constr2trl  23321  crcts  23331  cycls  23332  constr3trllem5  23363  constr3cycllem1  23367  constr3cyclp  23371  3v3e3cycl  23374  4cycl4v4e  23375  4cycl4dv4e  23377  eupatrl  23412  grpoidinvlem4  23517  grpoideu  23519  grpoidinv2  23528  rngo2  23698  blocnilem  24027  ipblnfi  24079  minvecolem4  24104  hvmul0or  24250  his35  24313  pjhtheu2  24642  3oalem2  24889  bralnfn  25175  kbpj  25183  eighmorth  25191  hmopm  25248  hmopco  25250  lnconi  25260  riesz3i  25289  cnlnadjlem6  25299  adjmul  25319  leopmuli  25360  nmopleid  25366  dmdbr2  25530  mdslmd1lem1  25552  superpos  25581  chirredlem2  25618  chirredi  25621  atcvat4i  25624  ifeqeqx  25726  iuninc  25735  abfmpeld  25793  fcobij  25849  fpwrelmap  25858  xaddeq0  25871  nndiffz1  25898  xreceu  25920  toslublem  25951  tosglblem  25953  xrsmulgzz  25962  abliso  25983  ogrpaddltbi  26006  ogrpinv0lt  26010  rge0srg  26064  gsumpropd2lem  26093  gsumle  26098  gsummpt2co  26101  gsumvsca1  26104  gsumvsca2  26105  orngsqr  26125  ofldchr  26135  xrge0slmod  26166  pstmxmet  26178  xpinpreima2  26191  sqsscirc2  26193  ordtconlem1  26208  xrge0iifiso  26219  elzrhunit  26262  qqhf  26269  qqhucn  26275  indpreima  26335  indf1ofs  26336  gsumesum  26364  esumlub  26365  esumpr2  26371  esumfzf  26372  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  sigainb  26433  insiga  26434  measiuns  26485  meascnbl  26487  measinb  26489  measdivcstOLD  26492  measdivcst  26493  dya2iocnrect  26550  dya2iocnei  26551  dya2iocucvr  26553  sibfof  26574  eulerpartlemf  26601  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemsima  26746  sgnmul  26773  sgnsub  26775  ccatmulgnn0dir  26788  ofs1  26791  ofcs1  26792  ofs2  26793  plymulx0  26796  signswch  26810  signstfvneq0  26821  signstfvcl  26822  signstfvc  26823  signstfveq0a  26825  signstfveq0  26826  gamcvg2lem  26893  subfacp1lem6  26921  pconcon  26968  conpcon  26972  sconpi1  26976  txscon  26978  cnllyscon  26982  cvmopnlem  27015  cvmfolem  27016  cvmlift  27036  sinccvg  27165  relexp0  27178  relexpindlem  27188  ntrivcvgmullem  27263  prodmolem2  27295  prodmo  27296  zprod  27297  fprod2dlem  27338  risefallfac  27374  fallfacfwd  27386  sltval2  27644  nodense  27677  nofulllem4  27693  btwncomim  27891  btwnswapid  27895  lineext  27954  btwnconn1lem11  27975  btwnconn1lem14  27978  broutsideof3  28004  outsideoftr  28007  outsidele  28010  ellines  28030  linethru  28031  lxflflp1  28265  heicant  28270  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  ismblfin  28276  itg2addnclem  28287  itg2addnclem2  28288  itg2addnc  28290  ftc1anclem5  28315  ftc1anclem7  28317  locfindis  28421  neibastop2lem  28425  neibastop2  28426  sdclem1  28483  geomcau  28499  isbnd3  28527  prdsbnd2  28538  ismtyhmeo  28548  heibor1  28553  rrnmet  28572  rrndstprj1  28573  rrncmslem  28575  rrncms  28576  iccbnd  28583  prter3  28872  elrfirn2  28877  mrefg3  28889  isnacs3  28891  mzprename  28931  rexrabdioph  28977  icodiamlt  29006  pellexlem3  29017  pellex  29021  pellqrex  29065  pellfundex  29072  pellfund14b  29085  monotoddzzfi  29128  rpexpmord  29134  jm2.24  29151  congsym  29156  acongtr  29166  bezoutr  29173  bezoutr1  29174  jm2.18  29182  harinf  29228  kelac1  29261  lnmlsslnm  29279  isnumbasgrplem3  29306  hbt  29331  dgraalem  29347  mpaaeu  29352  mendlmod  29395  acsfn1p  29401  proot1mul  29409  iocinico  29432  ofmul12  29444  ofdivdiv2  29447  refsumcn  29597  fmul01lt1lem1  29610  climsuselem1  29626  climsuse  29627  stoweidlem7  29648  stoweidlem14  29655  stoweidlem19  29660  stoweidlem20  29661  stoweidlem26  29667  stoweidlem31  29672  stoweidlem34  29675  stoweidlem39  29680  stoweidlem44  29685  stoweidlem46  29687  stoweidlem48  29689  stoweidlem59  29700  stoweidlem60  29701  stirlinglem5  29719  afvco2  29928  ndmaovdistr  29959  2f1fvneq  29989  imarnf1pr  29996  uzuzle  30036  elfz2z  30044  2elfz2melfz  30048  modfsummod  30091  powm2modprm  30094  lswn0  30104  usgra2pthspth  30141  wwlkiswwlkn  30182  vfwlkniswwlkn  30186  wlkiswwlksur  30197  wwlknext  30202  wwlkextfun  30207  wwlkexthasheq  30212  el2wlkonotot1  30239  usg2spthonot0  30254  usg2spthonot1  30255  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem1  30295  clwlkisclwwlk  30297  clwwlkf  30302  clwwlkf1  30304  clwwlkfo  30305  clwwlkvbij  30309  wwlkext2clwwlk  30311  clwwisshclwwlem  30316  hashecclwwlkn1  30354  usghashecclwwlk  30355  usgravd00  30384  wwlkextproplem2  30407  wwlkextproplem3  30408  wwlkextprop  30409  rusgranumwlks  30420  2pthfrgra  30449  frgrancvvdeqlemC  30478  frgrawopreglem4  30486  frrusgraord  30510  extwwlkfablem2  30517  numclwwlkovf2ex  30525  numclwwlkqhash  30539  numclwlk2lem2f1o  30544  numclwwlk6  30552  frgrareggt1  30555  scmsuppfi  30621  lincsumcl  30674  lcosslsp  30681  islinindfis  30692  lincext3  30699  ldepspr  30716  lincresunit2  30721  lincresunit3lem2  30723  isldepslvec2  30728  lmod1  30743  onfrALTlem2  30955  2pm13.193  30962  onfrALTlem2VD  31327  lssats  32230  lfl0f  32287  ncvr1  32490  cvrletrN  32491  cvrnrefN  32500  iscvlat2N  32542  ltltncvr  32640  atcvrj2b  32649  atltcvr  32652  cvrat4  32660  islln3  32727  llnle  32735  2at0mat0  32742  islpln3  32750  islpln5  32752  islpln2a  32765  islvol3  32793  pmapglb2N  32988  pmapglb2xN  32989  isline3  32993  isline4N  32994  pmod1i  33065  pclbtwnN  33114  pclfinN  33117  pexmidN  33186  pexmidlem8N  33194  lhplt  33217  lhpexle1  33225  lhpjat1  33237  lhpj1  33239  lhpmcvr  33240  lhpmcvr2  33241  lhpm0atN  33246  lautcvr  33309  ldil1o  33329  ldilcnv  33332  ltrn1o  33341  idltrn  33367  cdlemc3  33410  cdlemc4  33411  cdlemd1  33415  cdleme0cp  33431  cdleme0cq  33432  cdlemeulpq  33437  cdleme1  33444  cdleme2  33445  cdleme3b  33446  cdleme3c  33447  cdlemedb  33514  cdleme27a  33584  cdlemefrs32fva  33617  cdleme42keg  33703  cdleme42mgN  33705  cdleme48gfv  33754  cdlemf2  33779  cdlemg1cex  33805  cdlemg5  33822  cdlemg4c  33829  trlcoat  33940  tgrpgrplem  33966  tendodi1  34001  tendodi2  34002  tendo0pl  34008  tendoicl  34013  tendoipl  34014  tendo0mul  34043  tendo0mulr  34044  dva1dim  34202  erngdvlem4  34208  erngdvlem4-rN  34216  tendospdi1  34238  dialss  34264  diaglbN  34273  diameetN  34274  dibglbN  34384  dib1dim2  34386  diblss  34388  dicssdvh  34404  diclss  34411  diclspsn  34412  dihlsscpre  34452  dihglblem5aN  34510  dihglblem4  34515  dihglblem5  34516  dih1dimatlem  34547  dihlsprn  34549  dihatlat  34552  dihglblem6  34558  dochvalr  34575
  Copyright terms: Public domain W3C validator