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

Theorem 3eqtrd 2466
Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
Hypotheses
Ref Expression
3eqtrd.1  |-  ( ph  ->  A  =  B )
3eqtrd.2  |-  ( ph  ->  B  =  C )
3eqtrd.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtrd  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2  |-  ( ph  ->  A  =  B )
2 3eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
3 3eqtrd.3 . . 3  |-  ( ph  ->  C  =  D )
42, 3eqtrd 2462 . 2  |-  ( ph  ->  B  =  D )
51, 4eqtrd 2462 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  tpeq123d  3885  diftpsn3  3924  oteq123d  3986  resiima  5206  fvun  5779  fvmptd  5796  offval  6298  ofval  6300  onoviun  6591  tz7.44-2  6651  seqomlem4  6696  om1  6771  oe1  6773  oarec  6791  nnm1  6877  cantnff  7613  cantnf0  7614  cantnfp1lem1  7618  cantnfp1lem3  7620  cantnflem3  7631  rankonidlem  7738  rankopb  7762  dfac12lem1  8007  ackbij1lem18  8101  hsmexlem5  8294  axcc3  8302  addpqnq  8799  mulpqnq  8802  mulidnq  8824  recmulnq  8825  prlem934  8894  axrnegex  9021  addid1  9230  cnegex  9231  addcan2  9235  addsub  9300  subsub2  9313  negsubdi2  9344  muladd  9450  mulsub  9460  recextlem1  9636  muleqadd  9650  divrec  9678  div23  9681  div12  9684  divcan7  9707  conjmul  9715  cru  9976  nndivtr  10025  uzindOLD  10348  xnegneg  10784  rexsub  10803  xnegid  10806  xposdif  10825  xmulpnf1  10837  xlemul1  10853  fseq1p1m1  11105  fldiv  11224  zmod10  11247  modcyc  11259  modmul12d  11263  modadd12d  11265  uzrdgsuci  11283  seqeq123d  11315  seqf1olem2  11346  seqid  11351  seqhomo  11353  expneg  11372  expmulz  11409  expdiv  11413  binom3  11483  discr  11499  bcn1  11587  bcnp1n  11588  bcval5  11592  bcn2m1  11598  bcn2p1  11599  hashbclem  11684  hashf1lem2  11688  ccatlen  11727  swrd0len  11752  ccatswrd  11756  spllen  11766  splfv1  11767  splfv2a  11768  splval2  11769  wrdeqcats1  11771  wrdind  11774  revlen  11777  s2prop  11844  s4prop  11845  crim  11903  remullem  11916  remul2  11918  immul2  11925  ipcnval  11931  cjreim  11948  resqrex  12039  sqrneglem  12055  absid  12084  abs1m  12122  sqreulem  12146  amgm2  12156  rlimno1  12430  iseraltlem2  12459  iseraltlem3  12460  iseralt  12461  fsump1i  12536  fsum2dlem  12537  fsumshftm  12547  ackbijnn  12590  binomlem  12591  binom1dif  12595  incexclem  12599  incexc  12600  incexc2  12601  climcndslem2  12613  harmonic  12621  arisum  12622  geo2sum  12633  geo2sum2  12634  cvgrat  12643  mertenslem1  12644  ef0lem  12664  eftlub  12693  efsep  12694  effsumlt  12695  tanval2  12717  efi4p  12721  resin4p  12722  recos4p  12723  tanhlt1  12744  efeul  12746  sinadd  12748  cosadd  12749  sinmul  12756  ef01bndlem  12768  absef  12781  demoivreALT  12785  rpnnen2lem11  12807  dvds2ln  12863  sadcp1  12950  bitsres  12968  smupp1  12975  smupvallem  12978  smueqlem  12985  smumullem  12987  eucalginv  13058  eucalg  13061  zgcdsq  13128  qden1elz  13132  phiprmpw  13148  eulerthlem1  13153  prmdiv  13157  odzdvds  13164  opeo  13170  pythagtriplem12  13183  iserodd  13192  pcqmul  13210  pcaddlem  13240  pcadd  13241  pcadd2  13242  pcmpt  13244  pcmpt2  13245  prmreclem4  13270  prmreclem5  13271  mul4sqlem  13304  4sqlem11  13306  4sqlem17  13312  vdwlem6  13337  vdwlem8  13339  ram0  13373  ramz  13376  ramub1lem2  13378  ramcl  13380  pwsvscafval  13699  sectco  13965  rescabs  14016  cofucl  14068  resf1st  14074  fuccocl  14144  invfuc  14154  homadm  14178  homacd  14179  prf1st  14284  prf2nd  14285  1st2ndprf  14286  evlfcllem  14301  evlfcl  14302  uncf1  14316  uncf2  14317  curfuncf  14318  diag11  14323  diag12  14324  diag2  14325  hofcllem  14338  hofcl  14339  yon11  14344  yon12  14345  yon2  14346  yonedalem21  14353  yonedalem22  14358  yonedalem3b  14359  yonedainv  14361  latj4rot  14514  cnvps  14627  spwpr4  14646  mhmco  14745  pwsdiagmhm  14751  pwsco1mhm  14752  pwsco2mhm  14753  gsumws1  14768  gsumws2  14771  gsumspl  14772  frmdup2  14793  grpinvid2  14837  grpinvadd  14850  grpsubid1  14857  grpsubadd  14859  grppncan  14862  mulgdirlem  14897  mulgneg2  14900  nmzsubg  14964  divsinv  14982  divssub  14983  conjnmz  15022  gaorber  15068  gastacl  15069  symginv  15088  lactghmga  15090  cntzsubm  15117  gsumwrev  15145  odnncl  15166  odmod  15167  odinv  15180  gexdvdsi  15200  gexdvds  15201  sylow1lem1  15215  sylow2blem3  15239  efgmnvl  15329  efginvrel2  15342  efgsval2  15348  efgsfo  15354  efgredleme  15358  efgredlemd  15359  efgredlemc  15360  efgredlem  15362  frgpinv  15379  vrgpinv  15384  frgpuplem  15387  frgpup1  15390  frgpup2  15391  ablsub2inv  15418  abladdsub4  15421  abladdsub  15422  ablpncan2  15423  ablpnpcan  15427  ablnncan  15428  invghm  15436  gex2abl  15449  gexexlem  15450  oddvdssubg  15453  gsumval3a  15495  gsumzaddlem  15509  gsumzmhm  15516  gsumzinv  15523  gsumsn  15526  gsum2d2lem  15530  dmdprdsplitlem  15578  dprd2db  15584  dpjidcl  15599  ablfac1eulem  15613  ablfac1eu  15614  pgpfac1lem2  15616  pgpfaclem1  15622  ablfaclem2  15627  rngm2neg  15690  dvr1  15777  dvrcan3  15780  abvneg  15905  pwsdiaglmhm  16116  lsppr0  16147  lspsneleq  16170  lspdisj  16180  lspfixed  16183  asclmul1  16381  asclmul2  16382  psrlidm  16450  psrridm  16451  mplsubglem  16481  mpllsslem  16482  mplsubrglem  16485  mplmonmul  16510  mplmon2  16536  mplascl  16539  mplmon2mul  16544  psropprmul  16615  coe1tm  16648  coe1tmfv2  16650  coe1tmmul2  16651  coe1tmmul2fv  16653  coe1pwmulfv  16655  ply1scl0  16664  ply1coe  16667  cnsubrg  16742  ip2di  16855  ip2subdi  16858  ocvlss  16882  lsmcss  16902  ptcld  17628  cnextfres  18082  tgphaus  18129  tgptsmscls  18162  ressuss  18276  xpsdsval  18394  imasf1oxms  18502  tmsxpsval2  18552  ngptgp  18660  tngnm  18675  nrginvrcnlem  18709  nmoi2  18747  xrsxmet  18823  recld2  18828  reperflem  18832  reconnlem2  18841  phtpycom  18996  pcoass  19032  pi1inv  19060  pi1cof  19067  pi1coghm  19069  nmoleub2lem3  19106  nmoleub3  19110  cphsubrglem  19123  ipcau2  19174  csscld  19186  cmetss  19250  bcth3  19267  pjthlem1  19321  ovolunlem1a  19375  ovolunlem1  19376  ovolicc2lem4  19399  volinun  19423  voliunlem1  19427  volsup  19433  uniioovol  19454  uniioombllem3  19460  uniioombllem4  19461  uniioombllem5  19462  dyadovol  19468  volivth  19482  mbflimsup  19541  i1faddlem  19568  itg1addlem4  19574  itg1addlem5  19575  mbfi1fseqlem6  19595  itg2const2  19616  itgcnlem  19664  itgrevallem1  19669  itgposval  19670  itgitg1  19683  itgaddlem2  19698  iblmulc2  19705  itgmulc2lem2  19707  itgmulc2  19708  itgabs  19709  itgspliticc  19711  ditgsplit  19731  dvcmul  19813  dvexp  19822  dvmptres2  19831  dvmptcmul  19833  dvexp3  19845  dvlip2  19862  dv11cn  19868  lhop1lem  19880  dvfsumlem2  19894  ftc1lem4  19906  ftc2  19911  ftc2ditg  19913  itgparts  19914  itgsubstlem  19915  evlslem3  19918  evlslem1  19919  evl1sca  19933  evl1var  19935  evl1addd  19937  evl1subd  19938  evl1muld  19939  pf1mpf  19955  tdeglem4  19966  mdegvscale  19981  mdegmullem  19984  coe1mul3  20005  deg1add  20009  deg1sublt  20016  deg1mul3le  20022  uc1pmon1p  20057  ply1remlem  20068  ply1rem  20069  fta1glem2  20072  fta1g  20073  plypf1  20114  dgradd2  20169  dgrmulc  20172  dgrcolem2  20175  dvply1  20184  plydivlem4  20196  fta1lem  20207  vieta1lem1  20210  vieta1lem2  20211  vieta1  20212  aareccl  20226  geolim3  20239  aaliou2b  20241  tayl0  20261  taylply2  20267  taylthlem1  20272  ulmshft  20289  radcnv0  20315  dvradcnv  20320  pserulm  20321  psercn  20325  pserdvlem2  20327  pserdv  20328  abelthlem7  20337  abelth  20340  ef2kpi  20369  sinhalfpip  20383  sinhalfpim  20384  coshalfpim  20386  ptolemy  20387  tangtx  20396  tanabsge  20397  pige3  20408  sineq0  20412  resinf1o  20421  tanregt0  20424  efif1olem2  20428  efif1olem4  20430  eff1olem  20433  logrnaddcl  20455  logneg  20465  eflogeq  20479  cosargd  20486  logimul  20492  logneg2  20493  tanarg  20497  logcnlem4  20519  logcn  20521  advlogexp  20529  logtayl  20534  cxpsqrlem  20576  cxpsqr  20577  dvcxp1  20609  dvcxp2  20610  cxpcn3  20615  sqrcn  20617  abscxpbnd  20620  root1cj  20623  cxpeq  20624  cosangneg2d  20632  ang180lem1  20634  lawcos  20641  pythag  20642  isosctrlem2  20646  isosctrlem3  20647  chordthmlem4  20659  dcubic1lem  20666  dcubic2  20667  dcubic1  20668  dcubic  20669  mcubic  20670  cubic2  20671  binom4  20673  dquartlem1  20674  dquartlem2  20675  dquart  20676  quart1lem  20678  quart1  20679  quartlem1  20680  asinlem2  20692  asinneg  20709  sinasin  20712  cosacos  20713  asinsinlem  20714  asinsin  20715  cosasin  20727  atancj  20733  efiatan  20735  atanlogsublem  20738  efiatan2  20740  2efiatan  20741  cosatan  20744  atantan  20746  dvatan  20758  atantayl  20760  atantayl2  20761  log2cnv  20767  log2tlbnd  20768  rlimcnp  20787  efrlim  20791  cxp2limlem  20797  jensen  20810  amgmlem  20811  amgm  20812  emcllem5  20821  wilthlem1  20834  wilthlem2  20835  ftalem5  20842  basellem2  20847  basellem3  20848  basellem4  20849  basellem5  20850  basellem8  20853  vmappw  20882  0sgm  20910  chtprm  20919  ppidif  20929  fsumdvdscom  20953  muinv  20961  fsumdvdsmul  20963  sgmppw  20964  0sgmppw  20965  1sgm2ppw  20967  chtublem  20978  chtub  20979  vmasum  20983  logfac2  20984  chpval2  20985  logfacrlim  20991  logexprlim  20992  perfectlem1  20996  perfectlem2  20997  perfect  20998  dchrsum2  21035  dchr2sum  21040  sum2dchr  21041  bposlem5  21055  bposlem9  21059  lgsval2lem  21073  lgsval4  21083  lgsval4a  21085  lgsneg  21086  lgsneg1  21087  lgsdir  21097  lgsne0  21100  lgsqrlem1  21108  lgseisenlem3  21118  lgseisenlem4  21119  lgsquadlem1  21121  lgsquadlem2  21122  lgsquad2lem1  21125  2sqlem3  21133  2sqblem  21144  chebbnd1lem1  21146  chebbnd1lem2  21147  chebbnd1  21149  rplogsumlem1  21161  rplogsumlem2  21162  rpvmasumlem  21164  dchrisumlem1  21166  dchrvmasumlem1  21172  dchrvmasumiflem1  21178  dchrvmasumiflem2  21179  dchrisum0flblem1  21185  rpvmasum2  21189  dchrisum0re  21190  rplogsum  21204  mudivsum  21207  mulogsum  21209  mulog2sumlem1  21211  mulog2sumlem2  21212  vmalogdivsum  21216  logsqvma  21219  selberg  21225  selberg2lem  21227  selberg2  21228  selberg3lem1  21234  selberg4lem1  21237  selberg4  21238  pntrmax  21241  pntrsumo1  21242  selbergr  21245  selberg34r  21248  pntsval2  21253  pntrlog2bndlem2  21255  pntrlog2bndlem4  21257  pntrlog2bndlem5  21258  pntpbnd1a  21262  pntpbnd2  21264  pntibndlem2  21268  pntlemb  21274  pntlemn  21277  pntlemr  21279  pntlemj  21280  pntlemf  21282  pntlemo  21284  pnt2  21290  ostth2  21314  ostth3  21315  cusgrasizeinds  21468  uvtxnm1nbgra  21486  1pthonlem1  21572  2pthlem2  21579  vdgr1d  21657  vdgr1a  21660  grpoinvid2  21802  grpoasscan2  21809  grpoinvop  21812  grpoinvdiv  21816  grpopncan  21822  grpopnpcan2  21824  gxpval  21830  gxnval  21831  gxmul  21849  gxmodid  21850  ablomuldiv  21860  ablonncan  21865  gxdi  21867  ablomul  21926  vcnegsubdi2  22037  vcoprne  22041  nvnegneg  22115  nvsubadd  22119  nvnncan  22127  nvdif  22137  nvpi  22138  nvabs  22145  nvge0  22146  nvnd  22163  imsmetlem  22165  dipcj  22196  0lno  22274  blocnilem  22288  ipasslem4  22318  ipasslem5  22319  ubthlem2  22356  htthlem  22403  hvpncan  22524  hvaddsub4  22563  his5  22571  his2sub  22577  bcsiALT  22664  norm1  22734  hhssmetdval  22761  pjhthlem1  22876  pjspansn  23062  cm2j  23105  5oalem2  23140  3oalem2  23148  mayete3i  23213  mayete3iOLD  23214  hoaddid1i  23272  honegsubdi2  23297  hoaddsub  23302  unoplin  23406  counop  23407  hmoplin  23428  hmopco  23509  riesz3i  23548  cnlnadjlem7  23559  adjcoi  23586  kbass2  23603  kbass6  23607  opsqrlem1  23626  hmopidmpji  23638  pjssposi  23658  pjclem4  23685  strlem1  23736  chirredlem2  23877  iuninc  23994  fmptpr  24045  xaddeq0  24102  xdivrec  24156  xrge0npcan  24199  gsumsn2  24202  rdivmuldivd  24210  dvrcan5  24212  kerunit  24244  metideq  24271  pstmfval  24274  xrge0iifhom  24306  xrge0iif1  24307  zrhnm  24336  zrhunitpreima  24345  qqhval2  24349  qqhghm  24355  qqhrhm  24356  qqhcn  24358  qqhucn  24359  qqhre  24369  logbrec  24388  esumsn  24439  esumpr  24440  esumpinfval  24446  esumpinfsum  24450  esummulc2  24455  hasheuni  24458  measun  24548  sibfof  24637  probfinmeasb  24670  cndprobtot  24677  cndprobnul  24678  orvcval2  24699  dstrvval  24711  dstrvprob  24712  ballotlemfp1  24732  ballotlemfmpn  24735  ballotlemsi  24755  zetacvg  24782  lgamgulmlem2  24797  lgamgulmlem3  24798  lgamcvg2  24822  gamp1  24825  subfacp1lem5  24853  subfacp1lem6  24854  subfacval2  24856  subfaclim  24857  m1expevenALT  24888  txsconlem  24910  cvxscon  24913  cvmliftlem5  24959  cvmliftlem10  24964  cvmliftlem11  24965  cvmliftlem13  24966  cvmlift2lem12  24984  cvmliftphtlem  24987  ghomf1olem  25088  modaddabs  25098  clim2prod  25200  ntrivcvgfvn0  25211  fprodser  25259  fprodefsum  25282  fprodeq0  25283  fprod2dlem  25288  iprodefisum  25302  risefacval2  25310  fallfacval2  25311  fallfacval3  25312  risefac1  25333  fallfac1  25334  0fallfac  25337  0risefac  25338  binomfallfaclem2  25340  fallfacfac  25345  faclimlem1  25346  gcdabsorb  25355  brbtwn2  25787  colinearalglem1  25788  colinearalglem4  25791  axsegconlem9  25807  ax5seglem2  25811  axeuclidlem  25844  axcontlem7  25852  linethru  26030  bpolylem  26037  bpolysum  26042  bpolydiflem  26043  bpoly2  26046  bpoly3  26047  bpoly4  26048  fsumcube  26049  mblfinlem  26185  mblfinlem2  26186  itg2addnclem  26197  itg2addnclem2  26198  itg2addnc  26200  itgaddnclem2  26205  iblmulc2nc  26211  itgmulc2nclem2  26213  itgmulc2nc  26214  itgabsnc  26215  ftc1cnnclem  26219  areacirclem2  26223  areacirc  26229  upixp  26363  fdc  26381  heiborlem4  26455  heiborlem6  26457  iscringd  26541  keridl  26574  fninfp  26667  fndifnfp  26669  lcomfsup  26679  diophrw  26749  eldioph2lem1  26750  irrapxlem3  26819  irrapxlem5  26821  pellexlem2  26825  pellexlem6  26829  pell1234qrmulcl  26850  pell14qrgt0  26854  pell1234qrdich  26856  reglogexpbas  26892  rmxy1  26917  rmxy0  26918  rmym1  26930  rmxluc  26931  rmyluc  26932  rmxdbl  26934  rmydbl  26935  jm2.18  26991  jm2.19lem4  26995  jm2.22  26998  jm2.23  26999  jm2.25  27002  jm2.27c  27010  jm3.1lem2  27021  lmhmfgsplit  27094  dsmmsubg  27119  frlmvscaval  27141  frlmssuvc2  27157  frlmsslsp  27158  frlmup1  27160  frlmup2  27161  enfixsn  27167  islindf4  27218  indlcim  27220  hbtlem1  27237  dgrsub2  27249  mpaaeu  27265  rgspnval  27283  rngunsnply  27288  pmtrmvd  27308  symggen  27321  symgtrinv  27323  psgnunilem5  27327  psgnunilem2  27328  psgnunilem4  27330  mamulid  27368  mamurid  27369  matbas2  27385  hashgcdlem  27426  proot1hash  27429  proot1ex  27430  fmul01lt1lem1  27623  m1expeven  27634  clim1fr1  27636  climdivf  27647  itgsinexplem1  27657  itgsinexp  27658  stoweidlem3  27661  stoweidlem10  27668  stoweidlem11  27669  stoweidlem13  27671  stoweidlem22  27680  stoweidlem26  27684  stoweidlem36  27694  stoweidlem37  27695  stoweidlem38  27696  wallispilem4  27726  wallispi  27728  wallispi2lem1  27729  wallispi2lem2  27730  wallispi2  27731  stirlinglem1  27732  stirlinglem3  27734  stirlinglem4  27735  stirlinglem5  27736  stirlinglem6  27737  stirlinglem7  27738  stirlinglem8  27739  stirlinglem10  27741  stirlinglem14  27745  stirlinglem15  27746  sigarac  27751  sigaras  27754  sigarms  27755  sigarexp  27758  sigarperm  27759  sigarcol  27763  sharhght  27764  sigaradd  27765  cevathlem2  27767  afvres  27945  fzosplitsnm1  28033  swrdltnd  28042  swrdccatin12lem3  28066  swrdccat3b  28073  frisusgranb  28143  frg2woteq  28205  frghash2spot  28208  usgreghash2spotv  28211  usgreghash2spot  28214  sinh-conventional  28238  sgnp  28276  sgnn  28280  lsmsat  29537  lflsub  29596  lfladdcl  29600  lflvscl  29606  lkrlss  29624  eqlkr  29628  lkrlsp  29631  ldualvsdi1  29672  ldualvsdi2  29673  ldualgrplem  29674  ldualvsubval  29686  lkrin  29693  latmassOLD  29758  omlfh1N  29787  glbconN  29905  3atlem2  30012  lplnexllnN  30092  dalem24  30225  pmapat  30291  pmapmeet  30301  atmod4i1  30394  atmod4i2  30395  pol1N  30438  2polpmapN  30441  2polvalN  30442  poldmj1N  30456  polatN  30459  osumcllem3N  30486  lhpmcvr3  30553  ldilco  30644  trl0  30698  cdlemc1  30719  cdlemc6  30724  cdleme0cp  30742  cdleme0cq  30743  cdleme1  30755  cdleme4  30766  cdleme8  30778  cdleme9  30781  cdleme10  30782  cdleme11g  30793  cdleme20j  30846  cdleme22e  30872  cdleme22eALTN  30873  cdleme23b  30878  cdleme30a  30906  cdlemefrs32fva  30928  cdleme35b  30978  cdleme35e  30981  cdleme17d2  31023  cdleme48d  31063  cdlemg4  31145  cdlemg7aN  31153  cdlemg17f  31194  trlcoabs2N  31250  trlcolem  31254  tendo0pl  31319  erngset  31328  erngset-rN  31336  cdlemh1  31343  cdlemi1  31346  cdlemk20  31402  cdlemk40  31445  cdlemkid1  31450  cdlemkfid3N  31453  erngdvlem3  31518  erngdvlem4  31519  erngdvlem3-rN  31526  tendocnv  31550  dia0  31581  diameetN  31585  dia2dimlem3  31595  dia2dimlem4  31596  cdlemn3  31726  cdlemn9  31734  dihordlem7b  31744  dih1  31815  dihwN  31818  dihglbcpreN  31829  dihmeetcN  31831  dihmeetbclemN  31833  dihmeetlem4preN  31835  dihmeetlem13N  31848  dihmeet  31872  doch1  31888  doch2val2  31893  dihoml4c  31905  djhexmid  31940  djh01  31941  dihjat1  31958  lclkrlem2c  32038  lclkrlem2j  32045  lclkrlem2m  32048  lcfrlem1  32071  lcfrlem23  32094  lcd0v  32140  lcdvsubval  32147  mapdindp  32200  mapdpglem21  32221  baerlem3lem1  32236  baerlem5alem1  32237  baerlem5blem1  32238  baerlem5amN  32245  baerlem5bmN  32246  baerlem5abmN  32247  hdmap10  32372  hdmapsub  32379  hdmaprnlem6N  32386  hdmap14lem8  32407  hgmapmul  32427  hdmapinvlem3  32452  hdmapinvlem4  32453  hgmapvvlem1  32455  hdmapglem7b  32460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2423
  Copyright terms: Public domain W3C validator