Theorem 3eqtri 2769

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 2765	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2765	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  csbid  3912  csbconstg  3918  csbie  3934  un23  4174  in32  4230  dfnul4  4335  unvdif  4475  undif2  4477  undifabs  4478  difun2  4481  difdifdir  4492  dfif4  4541  dfif5  4542  tpidm23  4757  dfopif  4870  dfiunv2  5035  symdif0  5085  symdifid  5087  unidif0  5360  uniop  5520  xpun  5759  dfrn2  5899  dfdmf  5907  dfrnf  5961  res0  6001  resres  6010  xpssres  6036  dfima2  6080  imai  6092  ima0  6095  imaundir  6170  xpima  6202  cnvrescnv  6215  dmresv  6220  rescnvcnv  6224  dmtpop  6238  rnsnopg  6241  resdmres  6252  resdifdi  6256  dmmpt  6260  dmco  6274  co01  6281  suc0  6459  iunsuc  6469  fresaun  6779  dffv4  6903  fvssunirnOLD  6940  f1ossf1o  7148  fpr  7174  mpo0  7518  dmoprab  7536  rnoprab  7538  elrnmpores  7571  ov6g  7597  1st0  8020  2nd0  8021  dfmpo  8127  curry1  8129  curry2  8132  fpar  8141  dftpos2  8268  tposoprab  8287  tposmpo  8288  fvmpocurryd  8296  frrlem14  8324  dfwrecsOLD  8338  wfrlem14OLD  8362  wfrlem16OLD  8364  dfrecs3  8412  dfrecs3OLD  8413  tfrlem8  8424  seqomlem3  8492  df2o3  8514  nlim2  8528  omxpenlem  9113  dfsdom2  9136  pwfir  9355  marypha2lem2  9476  sup00  9504  epinid0  9640  scottexs  9927  scott0s  9928  infxpenc2  10062  kmlem3  10193  ackbij1lem2  10260  compsscnv  10411  fin1a2lem12  10451  mulerpqlem  10995  1lt2nq  11013  axi2m1  11199  2p2e4  12401  numsuc  12747  numsucc  12773  decmul10add  12802  5p5e10  12804  6p4e10  12805  7p3e10  12808  xnegmnf  13252  pnfaddmnf  13272  fz12pr  13621  fz0tp  13668  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  fzo13pr  13788  fzo0to2pr  13789  fz01pr  13790  fzo0to3tp  13791  fzo0to42pr  13792  fzo1to4tp  13793  fldiv4p1lem1div2  13875  sq4e2t8  14238  i4  14243  crreczi  14267  fac1  14316  fac3  14319  hashkf  14371  hashinf  14374  dmhashres  14380  hashun3  14423  cshwsexaOLD  14863  dmtrclfv  15057  abs0  15324  absi  15325  trirecip  15899  geoihalfsum  15918  esum  16116  tan0  16187  coshval  16191  ef01bndlem  16220  3dvds  16368  3dvdsdec  16369  3dvds2dec  16370  sadc0  16491  3lcm2e6woprm  16652  6lcm4e12  16653  lcmf0  16671  prmo0  17074  gcdmodi  17112  karatsuba  17121  43prm  17159  139prm  17161  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  setsfun  17208  setsfun0  17209  ndxarg  17233  pmtrsn  19537  psgnprfval1  19540  sylow2a  19637  ablfac1eu  20093  sralem  21175  sralemOLD  21176  pzriprng1ALT  21507  opsrtoslem2  22080  ply1plusgfvi  22243  pf1rcl  22353  restcld  23180  neitr  23188  txbasval  23614  txindis  23642  cnmpt1st  23676  cnmpt2nd  23677  ufildr  23939  restmetu  24583  cphipval2  25275  reust  25415  ehl0base  25450  ismbl  25561  mbfimaopnlem  25690  itg10  25723  itg2cnlem2  25797  itgz  25816  dvmptid  25995  cos2pi  26518  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  pige3ALT  26562  dfrelog  26607  logm1  26631  dvlog  26693  efopnlem2  26699  cxpexp  26710  root1id  26797  sqrt2cxp2logb9e3  26842  ang180lem2  26853  1cubrlem  26884  quart1  26899  atandm2  26920  efiasin  26931  asinsinlem  26934  asinsin  26935  asin1  26937  acos1  26938  atancj  26953  atanlogsublem  26958  efiatan2  26960  2efiatan  26961  tanatan  26962  dvatan  26978  log2cnv  26987  log2ublem2  26990  log2ublem3  26991  birthday  26997  basellem8  27131  cht1  27208  chp1  27210  ppi1i  27211  ppi2i  27212  cht2  27215  cht3  27216  bclbnd  27324  bposlem8  27335  2lgslem3c  27442  2lgslem3d  27443  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem4  27785  bday0s  27873  old0  27898  new0  27913  left1s  27933  right1s  27934  sltlpss  27945  slelss  27946  mulsproplem13  28154  mulsproplem14  28155  precsexlem1  28231  precsexlem2  28232  ax5seglem7  28950  axlowdimlem8  28964  axlowdimlem11  28967  vtxvalsnop  29058  iedgvalsnop  29059  umgrislfupgrlem  29139  usgrexmpledg  29279  usgredgffibi  29341  vdegp1bi  29555  edginwlk  29653  uhgrwkspthlem2  29774  clwwlkvbij  30132  wlk2v2elem2  30175  frgrwopreglem3  30333  ex-dif  30442  ex-xp  30455  ex-rn  30459  ex-lcm  30477  ex-prmo  30478  ip0i  30844  ip1ilem  30845  ipdirilem  30848  ipasslem10  30858  hvnegdii  31081  hvaddcani  31084  hvsubaddi  31085  hisubcomi  31123  normlem0  31128  normlem3  31131  normlem9  31137  bcseqi  31139  norm0  31147  norm-ii-i  31156  norm3difi  31166  normpari  31173  normpar2i  31175  polid2i  31176  shs0i  31468  chj0i  31474  pjsslem  31698  ho0subi  31814  hoaddsubi  31840  hosd1i  31841  hopncani  31843  nmop0  32005  nmfn0  32006  lnopunilem1  32029  lnophmlem2  32036  opsqrlem2  32160  pjclem1  32214  atabsi  32420  dmdbr6ati  32442  inin  32535  iuninc  32573  gtiso  32710  f1od2  32732  fpwrelmapffs  32745  fzodif1  32794  nn0split01  32819  dfdec100  32832  dp20u  32860  dp3mul10  32880  dpmul1000  32881  dpexpp1  32890  dpadd2  32892  dpmul  32895  dpmul4  32896  1mhdrd  32898  cycpmrn  33163  tocyccntz  33164  lmat22det  33821  ordtcnvNEW  33919  ordtrest2NEW  33922  zlmtset  33963  zlmtsetOLD  33964  qqhucn  33993  esumnul  34049  mbfmcst  34261  carsggect  34320  eulerpartgbij  34374  eulerpartlemn  34383  fib0  34401  fib1  34402  fib2  34404  fib3  34405  fib4  34406  fib5  34407  fib6  34408  0rrv  34453  coinflipprob  34482  ballotlem2  34491  ballotth  34540  signsvf0  34595  itgexpif  34621  hgt750lem  34666  hgt750lem2  34667  bnj1416  35053  derang0  35174  subfac0  35182  subfac1  35183  satfv1  35368  fmla  35386  fmla0  35387  fmla0xp  35388  fmla1  35392  mthmpps  35587  problem2  35671  quad3  35675  dfrdg2  35796  pprodcnveq  35884  dffv5  35925  fullfunfv  35948  ellines  36153  rankeq1o  36172  onint1  36450  bj-xpimasn  36956  bj-pr11val  37006  bj-pr21val  37014  bj-pr22val  37020  bj-nuliotaALT  37059  bj-dfmpoa  37119  bj-opabco  37189  icorempo  37352  finxpreclem4  37395  finxp2o  37400  finxp3o  37401  matunitlindf  37625  poimirlem5  37632  poimirlem22  37649  poimirlem26  37653  poimirlem30  37657  ismblfin  37668  dvtan  37677  asindmre  37710  dvasin  37711  dvacos  37712  areacirclem5  37719  heiborlem6  37823  xrnres4  38406  dfcoels  38431  coss0  38480  refsymrels2  38566  dfeqvrels2  38589  refrelsredund4  38633  hdmap1cbv  41804  lcm4un  42017  lcm5un  42018  lcm6un  42019  lcm7un  42020  lcm8un  42021  3lexlogpow5ineq1  42055  5bc2eq10  42143  2xp3dxp2ge1d  42242  imaopab  42270  decpmul  42323  cxpi11d  42379  tan3rdpi  42386  readvrec2  42391  remul02  42435  fltnltalem  42672  sum9cubes  42682  diophrw  42770  dnwech  43060  lmhmlnmsplit  43099  fgraphopab  43215  arearect  43227  areaquad  43228  oaomoencom  43330  dmnonrel  43603  imanonrel  43606  cononrel1  43607  cononrel2  43608  rclexi  43628  rtrclex  43630  dfrtrcl5  43642  sqrtcval  43654  resqrtvalex  43658  imsqrtvalex  43659  cnvtrrel  43683  dfrcl2  43687  dfrcl4  43689  iunrelexp0  43715  comptiunov2i  43719  relexpaddss  43731  brtrclfv2  43740  trclfvdecomr  43741  corcltrcl  43752  cotrclrcl  43755  fsovcnvlem  44026  neicvgnvo  44128  scottabf  44259  mnuprdlem1  44291  hashnzfz  44339  lhe4.4ex1a  44348  tgqioo2  45560  sumnnodd  45645  limsup0  45709  limsup10ex  45788  liminf10ex  45789  cosnegpi  45882  itgsin0pilem1  45965  stoweidlem13  46028  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem3  46091  dirkertrigeqlem1  46113  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  sqwvfoura  46243  fouriersw  46246  etransclem23  46272  etransclem36  46285  etransclem38  46287  carageniuncllem1  46536  0ome  46544  ovn02  46583  smflimlem4  46789  smflim  46792  smflim2  46821  smflimsup  46843  smfliminf  46846  fmtno0  47527  fmtno1  47528  fmtno2  47537  fmtno3  47538  fmtno4  47539  fmtno5lem4  47543  139prmALT  47583  31prm  47584  5tcu2e40  47602  3exp4mod41  47603  41prothprmlem2  47605  41prothprm  47606  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem1  47792  tgoldbachlt  47803  isuspgrim0lem  47871  isubgr3stgrlem4  47936  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  usgrexmpl1vtx  47982  usgrexmpl1edg  47983  usgrexmpl2vtx  47987  usgrexmpl2edg  47988  gpg5gricstgr3  48046  cznrnglem  48175  2t6m3t4e0  48264  zlmodzxzldeplem3  48419  ackval0  48601  ackval1  48602  ackval2  48603  ackval3  48604  ackval40  48614  ackval42  48617  ackval50  48619  disjdifb  48729  dftpos6  48775  tposresg  48778  tposrescnv  48779  tposres3  48781  tposid  48785  iscnrm3rlem1  48837  dfswapf2  48967  mndtchom  49181  sec0  49279