Theorem 3eqtri 2788

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	⊢ 𝐴 = 𝐵
3eqtri.2	⊢ 𝐵 = 𝐶
3eqtri.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtri	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3		3eqtri.3	. . 3 ⊢ 𝐶 = 𝐷
4	2, 3	eqtri 2784	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2784	1 ⊢ 𝐴 = 𝐷

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  csbid  3860  csbconstg  3866  csbie  3882  un23  4120  in32  4175  dfnul4  4281  unvdif  4429  undif2  4431  undifabs  4434  difun2  4437  difdifdir  4447  dfif4  4498  dfif5  4499  tpidm23  4718  dfopif  4830  dfiunv2  4992  symdif0  5045  symdifv  5046  symdifid  5047  unidif0  5321  unidif0OLD  5322  uniop  5488  xpun  5725  dfrn2  5870  dfdmf  5878  dfrnf  5932  res0  5974  resres  5983  xpssres  6007  dfima2  6058  imai  6072  ima0  6075  imaundir  6142  xpima  6174  cnvrescnv  6188  dmresv  6193  rescnvcnv  6204  dmtpop  6218  rnsnopg  6221  resdmres  6232  resdifdi  6236  dmmpt  6240  dmco  6255  co01  6262  relcnvtrg  6267  suc0  6439  iunsuc  6449  fresaun  6751  dffv4  6880  f1ossf1o  7127  fpr  7156  mpo0  7503  dmoprab  7521  rnoprab  7523  elrnmpores  7556  ov6g  7582  1st0  8005  2nd0  8006  dfmpo  8111  curry1  8113  curry2  8116  fpar  8125  dftpos2  8253  tposoprab  8272  tposmpo  8273  fvmpocurryd  8281  frrlem14  8310  dfrecs3  8373  tfrlem8  8385  seqomlem3  8455  df2o3  8477  nlim2  8491  omxpenlem  9090  dfsdom2  9112  pwfir  9301  marypha2lem2  9421  sup00  9450  epinid0  9592  scottabf  9932  scottexsOLD  9936  scott0bsOLD  9938  infxpenc2  10094  kmlem3  10224  ackbij1lem2  10291  compsscnv  10442  fin1a2lem12  10482  mulerpqlem  11033  1lt2nq  11051  axi2m1  11237  2p2e4  12470  numsuc  12821  numsucc  12852  decmul10add  12881  5p5e10  12883  6p4e10  12884  7p3e10  12887  xnegmnf  13333  pnfaddmnf  13353  fz12pr  13708  fz0tp  13755  fz0to3un2pr  13756  fz0to4untppr  13757  fz0to5un2tp  13758  fzo13pr  13877  fzo0to2pr  13878  fz01pr  13879  fzo0to3tp  13880  fzo0to42pr  13881  fzo1to4tp  13882  fldiv4p1lem1div2  13968  sq4e2t8  14335  i4  14341  crreczi  14365  fac1  14414  fac3  14417  hashkf  14469  hashinf  14472  dmhashres  14478  hashun3  14521  dmtrclfv  15164  abs0  15445  absi  15446  trirecip  16025  geoihalfsum  16044  esum  16239  tan0  16312  coshval  16316  ef01bndlem  16345  3dvds  16494  3dvdsdec  16495  3dvds2dec  16496  sadc0  16617  3lcm2e6woprm  16783  6lcm4e12  16784  lcmf0  16802  prmo0  17207  prmo3  17212  gcdmodi  17245  karatsuba  17254  43prm  17293  139prm  17295  631prm  17298  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  2503lem1  17308  2503lem2  17309  2503lem3  17310  4001lem1  17312  4001lem2  17313  4001lem3  17314  4001lem4  17315  setsfun  17342  setsfun0  17343  ndxarg  17367  chnccat  18793  ex-chn2  18805  pmtrsn  19726  psgnprfval1  19729  sylow2a  19826  ablfac1eu  20282  sralem  21444  pzriprng1ALT  21795  opsrtoslem2  22358  ply1plusgfvi  22552  pf1rcl  22660  matunitlindf  22989  restcld  23483  neitr  23491  txbasval  23918  txindis  23946  cnmpt1st  23980  cnmpt2nd  23981  ufildr  24243  restmetu  24882  cphipval2  25555  reust  25695  ehl0base  25730  ismbl  25840  mbfimaopnlem  25969  itg10  26002  itg2cnlem2  26076  itgz  26094  dvmptid  26270  cos2pi  26798  tan4thpi  26836  sincos6thpi  26837  pige3ALT  26841  dfrelog  26886  logm1  26910  dvlog  26972  efopnlem2  26978  cxpexp  26989  root1id  27075  sqrt2cxp2logb9e3  27120  ang180lem2  27131  1cubrlem  27162  quart1  27177  atandm2  27198  efiasin  27209  asinsinlem  27212  asinsin  27213  asin1  27215  acos1  27216  atancj  27231  atanlogsublem  27236  efiatan2  27238  2efiatan  27239  tanatan  27240  dvatan  27256  log2cnv  27265  log2ublem2  27268  log2ublem3  27269  birthday  27275  cht1  27485  chp1  27487  ppi1i  27488  ppi2i  27489  cht2  27492  cht3  27493  bclbnd  27600  bposlem8  27611  2lgslem3c  27718  2lgslem3d  27719  noetasuplem2  28084  noetasuplem3  28085  noetasuplem4  28086  noetainflem4  28090  bday0  28190  old0  28218  new0  28243  left1s  28274  right1s  28275  ltslpss  28287  leslss  28288  mulsproplem13  28507  mulsproplem14  28508  precsexlem1  28586  precsexlem2  28587  oniso  28650  bdayn0sf1o  28749  ax5seglem7  29506  axlowdimlem8  29520  axlowdimlem11  29523  vtxvalsnop  29612  iedgvalsnop  29613  umgrislfupgrlem  29693  usgrexmpledg  29836  usgredgffibi  29898  vdegp1bi  30111  edginwlk  30208  uhgrwkspthlem2  30333  clwwlkvbij  30697  wlk2v2elem2  30750  frgrwopreglem3  30908  ex-dif  31017  ex-xp  31030  ex-rn  31034  ex-lcm  31052  ex-prmo  31053  ip0i  31420  ip1ilem  31421  ipdirilem  31424  ipasslem10  31434  hvnegdii  31657  hvaddcani  31660  hvsubaddi  31661  hisubcomi  31699  normlem0  31704  normlem3  31707  normlem9  31713  bcseqi  31715  norm0  31723  norm-ii-i  31732  norm3difi  31742  normpari  31749  normpar2i  31751  polid2i  31752  shs0i  32044  chj0i  32050  pjsslem  32274  ho0subi  32390  hoaddsubi  32416  hosd1i  32417  hopncani  32419  nmop0  32581  nmfn0  32582  lnopunilem1  32605  lnophmlem2  32612  opsqrlem2  32736  pjclem1  32790  atabsi  32996  dmdbr6ati  33018  inin  33105  iuninc  33148  gtiso  33287  f1od2  33304  fpwrelmapffs  33319  fzodif1  33377  nn0split01  33402  dfdec100  33414  dp20u  33437  dp3mul10  33457  dpmul1000  33458  dpexpp1  33467  dpadd2  33469  dpmul  33472  dpmul4  33473  1mhdrd  33475  cycpmrn  33697  tocyccntz  33698  cos9thpiminplylem4  34410  cos9thpiminplylem5  34411  lmat22det  34447  ordtcnvNEW  34545  ordtrest2NEW  34548  zlmtset  34588  qqhucn  34617  esumnul  34673  mbfmcst  34884  carsggect  34943  eulerpartgbij  34997  eulerpartlemn  35006  fib0  35024  fib1  35025  fib2  35027  fib3  35028  fib4  35029  fib5  35030  fib6  35031  0rrv  35076  coinflipprob  35105  ballotlem2  35114  ballotth  35163  signsvf0  35202  itgexpif  35228  hgt750lem  35273  hgt750lem2  35274  bnj1416  35662  r11  35714  r12  35715  derang0  35913  subfac0  35921  subfac1  35922  satfv1  36107  fmla  36125  fmla0  36126  fmla0xp  36127  fmla1  36131  mthmpps  36326  problem2  36410  quad3  36414  dfrdg2  36537  pprodcnveq  36625  dffv5  36666  dfsuccf2  36685  fullfunfv  36691  ellines  36897  rankeq1o  36912  onint1  37217  bj-xpimasn  37848  bj-pr11val  37898  bj-pr21val  37906  bj-pr22val  37912  bj-nuliotaALT  37953  bj-dfmpoa  38019  bj-opabco  38089  icorempo  38254  finxpreclem4  38297  finxp2o  38302  finxp3o  38303  poimirlem5  38523  poimirlem22  38540  poimirlem26  38544  poimirlem30  38548  ismblfin  38559  dvtan  38568  asindmre  38601  dvasin  38602  dvacos  38603  areacirclem5  38610  heiborlem6  38730  dmcnvep  39300  dmxrncnvep  39301  dmcnvepres  39302  dmxrnuncnvepres  39304  xrnres4  39340  dfadjliftmap2  39369  blockadjliftmap  39370  dfblockliftmap2  39373  dfsucmap3  39375  dfsuccl2  39382  dfcoels  39432  coss0  39481  refsymrels2  39561  dfeqvrels2  39584  refrelsredund4  39628  hdmap1cbv  42839  lcm4un  43046  lcm5un  43047  lcm6un  43048  lcm7un  43049  lcm8un  43050  3lexlogpow5ineq1  43084  5bc2eq10  43172  imaopab  43265  decpmul  43325  cxpi11d  43374  tan3rdpi  43383  sin2t3rdpi  43384  cos2t3rdpi  43385  readvrec2  43392  remul02  43436  fltnltalem  43653  sum9cubes  43663  diophrw  43749  dnwech  44034  lmhmlnmsplit  44073  fgraphopab  44189  arearect  44201  areaquad  44202  oaomoencom  44303  dmnonrel  44575  imanonrel  44578  cononrel1  44579  cononrel2  44580  rclexi  44600  rtrclex  44602  dfrtrcl5  44614  sqrtcval  44626  resqrtvalex  44630  imsqrtvalex  44631  cnvtrrel  44655  dfrcl2  44659  dfrcl4  44661  iunrelexp0  44687  comptiunov2i  44691  relexpaddss  44703  brtrclfv2  44712  trclfvdecomr  44713  corcltrcl  44724  cotrclrcl  44727  fsovcnvlem  44998  neicvgnvo  45100  mnuprdlem1  45241  hashnzfz  45289  lhe4.4ex1a  45298  tgqioo2  46528  sumnnodd  46611  limsup0  46673  limsup10ex  46752  liminf10ex  46753  cosnegpi  46846  itgsin0pilem1  46929  stoweidlem13  46992  wallispilem4  47047  wallispi2lem1  47050  wallispi2lem2  47051  stirlinglem3  47055  dirkertrigeqlem1  47077  fourierdlem56  47141  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  sqwvfoura  47207  fouriersw  47210  etransclem23  47236  etransclem36  47249  etransclem38  47251  carageniuncllem1  47500  0ome  47508  ovn02  47547  smflimlem4  47753  smflim  47756  smflim2  47785  smflimsup  47807  smfliminf  47810  numtowerdt  47885  cos5t  47894  goldpolyfactor  47896  goldratmolem2  47902  goldratval  47905  cjnpoly  47908  fmtno0  48594  fmtno1  48595  fmtno2  48604  fmtno3  48605  fmtno4  48606  fmtno5lem4  48610  139prmALT  48650  31prm  48651  5tcu2e40  48669  3exp4mod41  48670  41prothprmlem2  48672  41prothprm  48673  ppivalnn4  48681  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbtbndlem1  48872  tgoldbachlt  48883  isuspgrim0lem  48960  isubgr3stgrlem4  49036  isubgr3stgrlem6  49038  isubgr3stgrlem7  49039  usgrexmpl1vtx  49090  usgrexmpl1edg  49091  usgrexmpl2vtx  49095  usgrexmpl2edg  49096  gpg5gricstgr3  49157  gpgprismgr4cycllem7  49168  cznrnglem  49325  2t6m3t4e0  49429  zlmodzxzldeplem3  49583  ackval0  49761  ackval1  49762  ackval2  49763  ackval3  49764  ackval40  49774  ackval42  49777  ackval50  49779  disjdifb  49889  dftpos6  49952  tposresg  49955  tposrescnv  49956  tposres3  49958  tposid  49962  iscnrm3rlem1  50017  dfswapf2  50338  setc1onsubc  50679  sec0  50822  dvcsc  50826  dvcot  50827