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

Theorem 3eqtrd 2440
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 2436 . 2  |-  ( ph  ->  B  =  D )
51, 4eqtrd 2436 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  tpeq123d  3858  diftpsn3  3897  oteq123d  3959  resiima  5179  fvun  5752  fvmptd  5769  offval  6271  ofval  6273  onoviun  6564  tz7.44-2  6624  seqomlem4  6669  om1  6744  oe1  6746  oarec  6764  nnm1  6850  cantnff  7585  cantnf0  7586  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem3  7603  rankonidlem  7710  rankopb  7734  dfac12lem1  7979  ackbij1lem18  8073  hsmexlem5  8266  axcc3  8274  addpqnq  8771  mulpqnq  8774  mulidnq  8796  recmulnq  8797  prlem934  8866  axrnegex  8993  addid1  9202  cnegex  9203  addcan2  9207  addsub  9272  subsub2  9285  negsubdi2  9316  muladd  9422  mulsub  9432  recextlem1  9608  muleqadd  9622  divrec  9650  div23  9653  div12  9656  divcan7  9679  conjmul  9687  cru  9948  nndivtr  9997  uzindOLD  10320  xnegneg  10756  rexsub  10775  xnegid  10778  xposdif  10797  xmulpnf1  10809  xlemul1  10825  fseq1p1m1  11077  fldiv  11196  zmod10  11219  modcyc  11231  modmul12d  11235  modadd12d  11237  uzrdgsuci  11255  seqeq123d  11287  seqf1olem2  11318  seqid  11323  seqhomo  11325  expneg  11344  expmulz  11381  expdiv  11385  binom3  11455  discr  11471  bcn1  11559  bcnp1n  11560  bcval5  11564  bcn2m1  11570  bcn2p1  11571  hashbclem  11656  hashf1lem2  11660  ccatlen  11699  swrd0len  11724  ccatswrd  11728  spllen  11738  splfv1  11739  splfv2a  11740  splval2  11741  wrdeqcats1  11743  wrdind  11746  revlen  11749  s2prop  11816  s4prop  11817  crim  11875  remullem  11888  remul2  11890  immul2  11897  ipcnval  11903  cjreim  11920  resqrex  12011  sqrneglem  12027  absid  12056  abs1m  12094  sqreulem  12118  amgm2  12128  rlimno1  12402  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  fsump1i  12508  fsum2dlem  12509  fsumshftm  12519  ackbijnn  12562  binomlem  12563  binom1dif  12567  incexclem  12571  incexc  12572  incexc2  12573  climcndslem2  12585  harmonic  12593  arisum  12594  geo2sum  12605  geo2sum2  12606  cvgrat  12615  mertenslem1  12616  ef0lem  12636  eftlub  12665  efsep  12666  effsumlt  12667  tanval2  12689  efi4p  12693  resin4p  12694  recos4p  12695  tanhlt1  12716  efeul  12718  sinadd  12720  cosadd  12721  sinmul  12728  ef01bndlem  12740  absef  12753  demoivreALT  12757  rpnnen2lem11  12779  dvds2ln  12835  sadcp1  12922  bitsres  12940  smupp1  12947  smupvallem  12950  smueqlem  12957  smumullem  12959  eucalginv  13030  eucalg  13033  zgcdsq  13100  qden1elz  13104  phiprmpw  13120  eulerthlem1  13125  prmdiv  13129  odzdvds  13136  opeo  13142  pythagtriplem12  13155  iserodd  13164  pcqmul  13182  pcaddlem  13212  pcadd  13213  pcadd2  13214  pcmpt  13216  pcmpt2  13217  prmreclem4  13242  prmreclem5  13243  mul4sqlem  13276  4sqlem11  13278  4sqlem17  13284  vdwlem6  13309  vdwlem8  13311  ram0  13345  ramz  13348  ramub1lem2  13350  ramcl  13352  pwsvscafval  13671  sectco  13937  rescabs  13988  cofucl  14040  resf1st  14046  fuccocl  14116  invfuc  14126  homadm  14150  homacd  14151  prf1st  14256  prf2nd  14257  1st2ndprf  14258  evlfcllem  14273  evlfcl  14274  uncf1  14288  uncf2  14289  curfuncf  14290  diag11  14295  diag12  14296  diag2  14297  hofcllem  14310  hofcl  14311  yon11  14316  yon12  14317  yon2  14318  yonedalem21  14325  yonedalem22  14330  yonedalem3b  14331  yonedainv  14333  latj4rot  14486  cnvps  14599  spwpr4  14618  mhmco  14717  pwsdiagmhm  14723  pwsco1mhm  14724  pwsco2mhm  14725  gsumws1  14740  gsumws2  14743  gsumspl  14744  frmdup2  14765  grpinvid2  14809  grpinvadd  14822  grpsubid1  14829  grpsubadd  14831  grppncan  14834  mulgdirlem  14869  mulgneg2  14872  nmzsubg  14936  divsinv  14954  divssub  14955  conjnmz  14994  gaorber  15040  gastacl  15041  symginv  15060  lactghmga  15062  cntzsubm  15089  gsumwrev  15117  odnncl  15138  odmod  15139  odinv  15152  gexdvdsi  15172  gexdvds  15173  sylow1lem1  15187  sylow2blem3  15211  efgmnvl  15301  efginvrel2  15314  efgsval2  15320  efgsfo  15326  efgredleme  15330  efgredlemd  15331  efgredlemc  15332  efgredlem  15334  frgpinv  15351  vrgpinv  15356  frgpuplem  15359  frgpup1  15362  frgpup2  15363  ablsub2inv  15390  abladdsub4  15393  abladdsub  15394  ablpncan2  15395  ablpnpcan  15399  ablnncan  15400  invghm  15408  gex2abl  15421  gexexlem  15422  oddvdssubg  15425  gsumval3a  15467  gsumzaddlem  15481  gsumzmhm  15488  gsumzinv  15495  gsumsn  15498  gsum2d2lem  15502  dmdprdsplitlem  15550  dprd2db  15556  dpjidcl  15571  ablfac1eulem  15585  ablfac1eu  15586  pgpfac1lem2  15588  pgpfaclem1  15594  ablfaclem2  15599  rngm2neg  15662  dvr1  15749  dvrcan3  15752  abvneg  15877  pwsdiaglmhm  16088  lsppr0  16119  lspsneleq  16142  lspdisj  16152  lspfixed  16155  asclmul1  16353  asclmul2  16354  psrlidm  16422  psrridm  16423  mplsubglem  16453  mpllsslem  16454  mplsubrglem  16457  mplmonmul  16482  mplmon2  16508  mplascl  16511  mplmon2mul  16516  psropprmul  16587  coe1tm  16620  coe1tmfv2  16622  coe1tmmul2  16623  coe1tmmul2fv  16625  coe1pwmulfv  16627  ply1scl0  16636  ply1coe  16639  cnsubrg  16714  ip2di  16827  ip2subdi  16830  ocvlss  16854  lsmcss  16874  ptcld  17598  cnextfres  18052  tgphaus  18099  tgptsmscls  18132  ressuss  18246  xpsdsval  18364  imasf1oxms  18472  tmsxpsval2  18522  ngptgp  18630  tngnm  18645  nrginvrcnlem  18679  nmoi2  18717  xrsxmet  18793  recld2  18798  reperflem  18802  reconnlem2  18811  phtpycom  18966  pcoass  19002  pi1inv  19030  pi1cof  19037  pi1coghm  19039  nmoleub2lem3  19076  nmoleub3  19080  cphsubrglem  19093  ipcau2  19144  csscld  19156  cmetss  19220  bcth3  19237  pjthlem1  19291  ovolunlem1a  19345  ovolunlem1  19346  ovolicc2lem4  19369  volinun  19393  voliunlem1  19397  volsup  19403  uniioovol  19424  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  dyadovol  19438  volivth  19452  mbflimsup  19511  i1faddlem  19538  itg1addlem4  19544  itg1addlem5  19545  mbfi1fseqlem6  19565  itg2const2  19586  itgcnlem  19634  itgrevallem1  19639  itgposval  19640  itgitg1  19653  itgaddlem2  19668  iblmulc2  19675  itgmulc2lem2  19677  itgmulc2  19678  itgabs  19679  itgspliticc  19681  ditgsplit  19701  dvcmul  19783  dvexp  19792  dvmptres2  19801  dvmptcmul  19803  dvexp3  19815  dvlip2  19832  dv11cn  19838  lhop1lem  19850  dvfsumlem2  19864  ftc1lem4  19876  ftc2  19881  ftc2ditg  19883  itgparts  19884  itgsubstlem  19885  evlslem3  19888  evlslem1  19889  evl1sca  19903  evl1var  19905  evl1addd  19907  evl1subd  19908  evl1muld  19909  pf1mpf  19925  tdeglem4  19936  mdegvscale  19951  mdegmullem  19954  coe1mul3  19975  deg1add  19979  deg1sublt  19986  deg1mul3le  19992  uc1pmon1p  20027  ply1remlem  20038  ply1rem  20039  fta1glem2  20042  fta1g  20043  plypf1  20084  dgradd2  20139  dgrmulc  20142  dgrcolem2  20145  dvply1  20154  plydivlem4  20166  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  aareccl  20196  geolim3  20209  aaliou2b  20211  tayl0  20231  taylply2  20237  taylthlem1  20242  ulmshft  20259  radcnv0  20285  dvradcnv  20290  pserulm  20291  psercn  20295  pserdvlem2  20297  pserdv  20298  abelthlem7  20307  abelth  20310  ef2kpi  20339  sinhalfpip  20353  sinhalfpim  20354  coshalfpim  20356  ptolemy  20357  tangtx  20366  tanabsge  20367  pige3  20378  sineq0  20382  resinf1o  20391  tanregt0  20394  efif1olem2  20398  efif1olem4  20400  eff1olem  20403  logrnaddcl  20425  logneg  20435  eflogeq  20449  cosargd  20456  logimul  20462  logneg2  20463  tanarg  20467  logcnlem4  20489  logcn  20491  advlogexp  20499  logtayl  20504  cxpsqrlem  20546  cxpsqr  20547  dvcxp1  20579  dvcxp2  20580  cxpcn3  20585  sqrcn  20587  abscxpbnd  20590  root1cj  20593  cxpeq  20594  cosangneg2d  20602  ang180lem1  20604  lawcos  20611  pythag  20612  isosctrlem2  20616  isosctrlem3  20617  chordthmlem4  20629  dcubic1lem  20636  dcubic2  20637  dcubic1  20638  dcubic  20639  mcubic  20640  cubic2  20641  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  asinlem2  20662  asinneg  20679  sinasin  20682  cosacos  20683  asinsinlem  20684  asinsin  20685  cosasin  20697  atancj  20703  efiatan  20705  atanlogsublem  20708  efiatan2  20710  2efiatan  20711  cosatan  20714  atantan  20716  dvatan  20728  atantayl  20730  atantayl2  20731  log2cnv  20737  log2tlbnd  20738  rlimcnp  20757  efrlim  20761  cxp2limlem  20767  jensen  20780  amgmlem  20781  amgm  20782  emcllem5  20791  wilthlem1  20804  wilthlem2  20805  ftalem5  20812  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  basellem8  20823  vmappw  20852  0sgm  20880  chtprm  20889  ppidif  20899  fsumdvdscom  20923  muinv  20931  fsumdvdsmul  20933  sgmppw  20934  0sgmppw  20935  1sgm2ppw  20937  chtublem  20948  chtub  20949  vmasum  20953  logfac2  20954  chpval2  20955  logfacrlim  20961  logexprlim  20962  perfectlem1  20966  perfectlem2  20967  perfect  20968  dchrsum2  21005  dchr2sum  21010  sum2dchr  21011  bposlem5  21025  bposlem9  21029  lgsval2lem  21043  lgsval4  21053  lgsval4a  21055  lgsneg  21056  lgsneg1  21057  lgsdir  21067  lgsne0  21070  lgsqrlem1  21078  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem1  21095  2sqlem3  21103  2sqblem  21114  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1  21119  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem1  21136  dchrvmasumlem1  21142  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  dchrisum0flblem1  21155  rpvmasum2  21159  dchrisum0re  21160  rplogsum  21174  mudivsum  21177  mulogsum  21179  mulog2sumlem1  21181  mulog2sumlem2  21182  vmalogdivsum  21186  logsqvma  21189  selberg  21195  selberg2lem  21197  selberg2  21198  selberg3lem1  21204  selberg4lem1  21207  selberg4  21208  pntrmax  21211  pntrsumo1  21212  selbergr  21215  selberg34r  21218  pntsval2  21223  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntlemb  21244  pntlemn  21247  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemo  21254  pnt2  21260  ostth2  21284  ostth3  21285  cusgrasizeinds  21438  uvtxnm1nbgra  21456  1pthonlem1  21542  2pthlem2  21549  vdgr1d  21627  vdgr1a  21630  grpoinvid2  21772  grpoasscan2  21779  grpoinvop  21782  grpoinvdiv  21786  grpopncan  21792  grpopnpcan2  21794  gxpval  21800  gxnval  21801  gxmul  21819  gxmodid  21820  ablomuldiv  21830  ablonncan  21835  gxdi  21837  ablomul  21896  vcnegsubdi2  22007  vcoprne  22011  nvnegneg  22085  nvsubadd  22089  nvnncan  22097  nvdif  22107  nvpi  22108  nvabs  22115  nvge0  22116  nvnd  22133  imsmetlem  22135  dipcj  22166  0lno  22244  blocnilem  22258  ipasslem4  22288  ipasslem5  22289  ubthlem2  22326  htthlem  22373  hvpncan  22494  hvaddsub4  22533  his5  22541  his2sub  22547  bcsiALT  22634  norm1  22704  hhssmetdval  22731  pjhthlem1  22846  pjspansn  23032  cm2j  23075  5oalem2  23110  3oalem2  23118  mayete3i  23183  mayete3iOLD  23184  hoaddid1i  23242  honegsubdi2  23267  hoaddsub  23272  unoplin  23376  counop  23377  hmoplin  23398  hmopco  23479  riesz3i  23518  cnlnadjlem7  23529  adjcoi  23556  kbass2  23573  kbass6  23577  opsqrlem1  23596  hmopidmpji  23608  pjssposi  23628  pjclem4  23655  strlem1  23706  chirredlem2  23847  iuninc  23964  fmptpr  24015  xaddeq0  24072  xdivrec  24126  xrge0npcan  24169  gsumsn2  24172  rdivmuldivd  24180  dvrcan5  24182  kerunit  24214  metideq  24241  pstmfval  24244  xrge0iifhom  24276  xrge0iif1  24277  zrhnm  24306  zrhunitpreima  24315  qqhval2  24319  qqhghm  24325  qqhrhm  24326  qqhcn  24328  qqhucn  24329  qqhre  24339  logbrec  24358  esumsn  24409  esumpr  24410  esumpinfval  24416  esumpinfsum  24420  esummulc2  24425  hasheuni  24428  measun  24518  sibfof  24607  probfinmeasb  24640  cndprobtot  24647  cndprobnul  24648  orvcval2  24669  dstrvval  24681  dstrvprob  24682  ballotlemfp1  24702  ballotlemfmpn  24705  ballotlemsi  24725  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamcvg2  24792  gamp1  24795  subfacp1lem5  24823  subfacp1lem6  24824  subfacval2  24826  subfaclim  24827  m1expevenALT  24858  txsconlem  24880  cvxscon  24883  cvmliftlem5  24929  cvmliftlem10  24934  cvmliftlem11  24935  cvmliftlem13  24936  cvmlift2lem12  24954  cvmliftphtlem  24957  ghomf1olem  25058  modaddabs  25068  clim2prod  25169  ntrivcvgfvn0  25180  fprodser  25228  fprodefsum  25251  fprodeq0  25252  fprod2dlem  25257  iprodefisum  25271  risefacval2  25279  fallfacval2  25280  risefac1  25299  fallfac1  25300  0fallfac  25304  0risefac  25305  binomfallfaclem2  25307  faclimlem1  25310  gcdabsorb  25319  brbtwn2  25748  colinearalglem1  25749  colinearalglem4  25752  axsegconlem9  25768  ax5seglem2  25772  axeuclidlem  25805  axcontlem7  25813  linethru  25991  bpolylem  25998  bpolysum  26003  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  itgaddnclem2  26163  iblmulc2nc  26169  itgmulc2nclem2  26171  itgmulc2nc  26172  itgabsnc  26173  ftc1cnnclem  26177  areacirclem2  26181  areacirc  26187  upixp  26321  fdc  26339  heiborlem4  26413  heiborlem6  26415  iscringd  26499  keridl  26532  fninfp  26625  fndifnfp  26627  lcomfsup  26637  diophrw  26707  eldioph2lem1  26708  irrapxlem3  26777  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell1234qrmulcl  26808  pell14qrgt0  26812  pell1234qrdich  26814  reglogexpbas  26850  rmxy1  26875  rmxy0  26876  rmym1  26888  rmxluc  26889  rmyluc  26890  rmxdbl  26892  rmydbl  26893  jm2.18  26949  jm2.19lem4  26953  jm2.22  26956  jm2.23  26957  jm2.25  26960  jm2.27c  26968  jm3.1lem2  26979  lmhmfgsplit  27052  dsmmsubg  27077  frlmvscaval  27099  frlmssuvc2  27115  frlmsslsp  27116  frlmup1  27118  frlmup2  27119  enfixsn  27125  islindf4  27176  indlcim  27178  hbtlem1  27195  dgrsub2  27207  mpaaeu  27223  rgspnval  27241  rngunsnply  27246  pmtrmvd  27266  symggen  27279  symgtrinv  27281  psgnunilem5  27285  psgnunilem2  27286  psgnunilem4  27288  mamulid  27326  mamurid  27327  matbas2  27343  hashgcdlem  27384  proot1hash  27387  proot1ex  27388  fmul01lt1lem1  27581  m1expeven  27592  clim1fr1  27594  climdivf  27605  itgsinexplem1  27615  itgsinexp  27616  stoweidlem3  27619  stoweidlem10  27626  stoweidlem11  27627  stoweidlem13  27629  stoweidlem22  27638  stoweidlem26  27642  stoweidlem36  27652  stoweidlem37  27653  stoweidlem38  27654  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem14  27703  stirlinglem15  27704  sigarac  27709  sigaras  27712  sigarms  27713  sigarexp  27716  sigarperm  27717  sigarcol  27721  sharhght  27722  sigaradd  27723  cevathlem2  27725  afvres  27903  fzosplitsnm1  27991  swrdltnd  28000  swrdccatin12lem3  28024  swrdccat3b  28031  frisusgranb  28101  frg2woteq  28163  frghash2spot  28166  usgreghash2spotv  28169  usgreghash2spot  28172  sinh-conventional  28196  sgnp  28234  sgnn  28238  lsmsat  29491  lflsub  29550  lfladdcl  29554  lflvscl  29560  lkrlss  29578  eqlkr  29582  lkrlsp  29585  ldualvsdi1  29626  ldualvsdi2  29627  ldualgrplem  29628  ldualvsubval  29640  lkrin  29647  latmassOLD  29712  omlfh1N  29741  glbconN  29859  3atlem2  29966  lplnexllnN  30046  dalem24  30179  pmapat  30245  pmapmeet  30255  atmod4i1  30348  atmod4i2  30349  pol1N  30392  2polpmapN  30395  2polvalN  30396  poldmj1N  30410  polatN  30413  osumcllem3N  30440  lhpmcvr3  30507  ldilco  30598  trl0  30652  cdlemc1  30673  cdlemc6  30678  cdleme0cp  30696  cdleme0cq  30697  cdleme1  30709  cdleme4  30720  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme11g  30747  cdleme20j  30800  cdleme22e  30826  cdleme22eALTN  30827  cdleme23b  30832  cdleme30a  30860  cdlemefrs32fva  30882  cdleme35b  30932  cdleme35e  30935  cdleme17d2  30977  cdleme48d  31017  cdlemg4  31099  cdlemg7aN  31107  cdlemg17f  31148  trlcoabs2N  31204  trlcolem  31208  tendo0pl  31273  erngset  31282  erngset-rN  31290  cdlemh1  31297  cdlemi1  31300  cdlemk20  31356  cdlemk40  31399  cdlemkid1  31404  cdlemkfid3N  31407  erngdvlem3  31472  erngdvlem4  31473  erngdvlem3-rN  31480  tendocnv  31504  dia0  31535  diameetN  31539  dia2dimlem3  31549  dia2dimlem4  31550  cdlemn3  31680  cdlemn9  31688  dihordlem7b  31698  dih1  31769  dihwN  31772  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbclemN  31787  dihmeetlem4preN  31789  dihmeetlem13N  31802  dihmeet  31826  doch1  31842  doch2val2  31847  dihoml4c  31859  djhexmid  31894  djh01  31895  dihjat1  31912  lclkrlem2c  31992  lclkrlem2j  31999  lclkrlem2m  32002  lcfrlem1  32025  lcfrlem23  32048  lcd0v  32094  lcdvsubval  32101  mapdindp  32154  mapdpglem21  32175  baerlem3lem1  32190  baerlem5alem1  32191  baerlem5blem1  32192  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  hdmap10  32326  hdmapsub  32333  hdmaprnlem6N  32340  hdmap14lem8  32361  hgmapmul  32381  hdmapinvlem3  32406  hdmapinvlem4  32407  hgmapvvlem1  32409  hdmapglem7b  32414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator