Theorem 3eqtri 2765

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  csbid  3906  csbconstg  3912  csbie  3929  un23  4168  in32  4221  dfnul4  4324  dfnul2OLD  4327  unvdif  4474  undif2  4476  undifabs  4477  difun2  4480  difdifdir  4491  dfif4  4543  dfif5  4544  tpidm23  4761  dfopif  4870  dfiunv2  5038  symdif0  5088  symdifid  5090  unidif0  5358  uniop  5515  xpun  5748  dfrn2  5887  dfdmf  5895  dfrnf  5948  res0  5984  resres  5993  xpssres  6017  dfima2  6060  imai  6071  ima0  6074  imaundir  6148  xpima  6179  cnvrescnv  6192  dmresv  6197  rescnvcnv  6201  dmtpop  6215  rnsnopg  6218  resdmres  6229  resdifdi  6233  dmmpt  6237  dmco  6251  co01  6258  suc0  6437  iunsuc  6447  fresaun  6760  dffv4  6886  fvssunirnOLD  6923  f1ossf1o  7123  fpr  7149  mpo0  7491  dmoprab  7507  rnoprab  7509  elrnmpores  7543  ov6g  7568  1st0  7978  2nd0  7979  dfmpo  8085  curry1  8087  curry2  8090  fpar  8099  dftpos2  8225  tposoprab  8244  tposmpo  8245  fvmpocurryd  8253  frrlem14  8281  dfwrecsOLD  8295  wfrlem14OLD  8319  wfrlem16OLD  8321  dfrecs3  8369  dfrecs3OLD  8370  tfrlem8  8381  seqomlem3  8449  df2o3  8471  nlim2  8487  omxpenlem  9070  dfsdom2  9093  pwfir  9173  marypha2lem2  9428  sup00  9456  epinid0  9592  scottexs  9879  scott0s  9880  infxpenc2  10014  kmlem3  10144  ackbij1lem2  10213  compsscnv  10363  fin1a2lem12  10403  mulerpqlem  10947  1lt2nq  10965  axi2m1  11151  2p2e4  12344  numsuc  12688  numsucc  12714  decmul10add  12743  5p5e10  12745  6p4e10  12746  7p3e10  12749  xnegmnf  13186  pnfaddmnf  13206  fz12pr  13555  fz0tp  13599  fz0to3un2pr  13600  fzo13pr  13713  fzo0to2pr  13714  fzo0to3tp  13715  fzo0to42pr  13716  fzo1to4tp  13717  fldiv4p1lem1div2  13797  sq4e2t8  14160  i4  14165  crreczi  14188  fac1  14234  fac3  14237  hashkf  14289  hashinf  14292  dmhashres  14298  hashun3  14341  cshwsexaOLD  14772  dmtrclfv  14962  abs0  15229  absi  15230  trirecip  15806  geoihalfsum  15825  esum  16021  tan0  16091  coshval  16095  ef01bndlem  16124  3dvds  16271  3dvdsdec  16272  3dvds2dec  16273  sadc0  16392  3lcm2e6woprm  16549  6lcm4e12  16550  lcmf0  16568  prmo0  16966  gcdmodi  17004  karatsuba  17014  43prm  17052  139prm  17054  631prm  17057  1259lem1  17061  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  2503lem1  17067  2503lem2  17068  2503lem3  17069  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  setsfun  17101  setsfun0  17102  ndxarg  17126  pmtrsn  19382  psgnprfval1  19385  sylow2a  19482  ablfac1eu  19938  sralem  20783  sralemOLD  20784  opsrtoslem2  21609  ply1plusgfvi  21756  pf1rcl  21860  restcld  22668  neitr  22676  txbasval  23102  txindis  23130  cnmpt1st  23164  cnmpt2nd  23165  ufildr  23427  restmetu  24071  cphipval2  24750  reust  24890  ehl0base  24925  ismbl  25035  mbfimaopnlem  25164  itg10  25197  itg2cnlem2  25272  itgz  25290  dvmptid  25466  cos2pi  25978  tan4thpi  26016  sincos6thpi  26017  pige3ALT  26021  dfrelog  26066  logm1  26089  dvlog  26151  efopnlem2  26157  cxpexp  26168  root1id  26252  sqrt2cxp2logb9e3  26294  ang180lem2  26305  1cubrlem  26336  quart1  26351  atandm2  26372  efiasin  26383  asinsinlem  26386  asinsin  26387  asin1  26389  acos1  26390  atancj  26405  atanlogsublem  26410  efiatan2  26412  2efiatan  26413  tanatan  26414  dvatan  26430  log2cnv  26439  log2ublem2  26442  log2ublem3  26443  birthday  26449  basellem8  26582  cht1  26659  chp1  26661  ppi1i  26662  ppi2i  26663  cht2  26666  cht3  26667  bclbnd  26773  bposlem8  26784  2lgslem3c  26891  2lgslem3d  26892  noetasuplem2  27227  noetasuplem3  27228  noetasuplem4  27229  noetainflem4  27233  bday0s  27319  old0  27344  new0  27359  left1s  27379  right1s  27380  sltlpss  27391  mulsproplem13  27574  mulsproplem14  27575  precsexlem1  27643  precsexlem2  27644  ax5seglem7  28183  axlowdimlem8  28197  axlowdimlem11  28200  vtxvalsnop  28291  iedgvalsnop  28292  umgrislfupgrlem  28372  usgrexmpledg  28509  usgredgffibi  28571  vdegp1bi  28784  edginwlk  28882  uhgrwkspthlem2  29001  clwwlkvbij  29356  wlk2v2elem2  29399  frgrwopreglem3  29557  ex-dif  29666  ex-xp  29679  ex-rn  29683  ex-lcm  29701  ex-prmo  29702  ip0i  30066  ip1ilem  30067  ipdirilem  30070  ipasslem10  30080  hvnegdii  30303  hvaddcani  30306  hvsubaddi  30307  hisubcomi  30345  normlem0  30350  normlem3  30353  normlem9  30359  bcseqi  30361  norm0  30369  norm-ii-i  30378  norm3difi  30388  normpari  30395  normpar2i  30397  polid2i  30398  shs0i  30690  chj0i  30696  pjsslem  30920  ho0subi  31036  hoaddsubi  31062  hosd1i  31063  hopncani  31065  nmop0  31227  nmfn0  31228  lnopunilem1  31251  lnophmlem2  31258  opsqrlem2  31382  pjclem1  31436  atabsi  31642  dmdbr6ati  31664  inin  31741  iuninc  31780  gtiso  31910  f1od2  31934  fpwrelmapffs  31947  fzodif1  31992  dfdec100  32024  dp20u  32032  dp3mul10  32052  dpmul1000  32053  dpexpp1  32062  dpadd2  32064  dpmul  32067  dpmul4  32068  1mhdrd  32070  cycpmrn  32290  tocyccntz  32291  lmat22det  32791  ordtcnvNEW  32889  ordtrest2NEW  32892  zlmtset  32933  zlmtsetOLD  32934  qqhucn  32961  esumnul  33035  mbfmcst  33247  carsggect  33306  eulerpartgbij  33360  eulerpartlemn  33369  fib0  33387  fib1  33388  fib2  33390  fib3  33391  fib4  33392  fib5  33393  fib6  33394  0rrv  33439  coinflipprob  33467  ballotlem2  33476  ballotth  33525  signsvf0  33580  itgexpif  33607  hgt750lem  33652  hgt750lem2  33653  bnj1416  34039  derang0  34149  subfac0  34157  subfac1  34158  satfv1  34343  fmla  34361  fmla0  34362  fmla0xp  34363  fmla1  34367  mthmpps  34562  problem2  34640  quad3  34644  dfrdg2  34756  pprodcnveq  34844  dffv5  34885  fullfunfv  34908  ellines  35113  rankeq1o  35132  onint1  35323  bj-xpimasn  35825  bj-pr11val  35875  bj-pr21val  35883  bj-pr22val  35889  bj-nuliotaALT  35928  bj-dfmpoa  35988  bj-opabco  36058  icorempo  36221  finxpreclem4  36264  finxp2o  36269  finxp3o  36270  matunitlindf  36475  poimirlem5  36482  poimirlem22  36499  poimirlem26  36503  poimirlem30  36507  ismblfin  36518  dvtan  36527  asindmre  36560  dvasin  36561  dvacos  36562  areacirclem5  36569  heiborlem6  36673  xrnres4  37264  dfcoels  37289  coss0  37338  refsymrels2  37424  dfeqvrels2  37447  refrelsredund4  37491  hdmap1cbv  40662  lcm4un  40870  lcm5un  40871  lcm6un  40872  lcm7un  40873  lcm8un  40874  3lexlogpow5ineq1  40908  5bc2eq10  40947  2xp3dxp2ge1d  41011  imaopab  41048  sqn5ii  41196  decpmul  41198  remul02  41275  fltnltalem  41401  diophrw  41483  dnwech  41776  lmhmlnmsplit  41815  fgraphopab  41938  arearect  41950  areaquad  41951  oaomoencom  42053  dmnonrel  42327  imanonrel  42330  cononrel1  42331  cononrel2  42332  rclexi  42352  rtrclex  42354  dfrtrcl5  42366  sqrtcval  42378  resqrtvalex  42382  imsqrtvalex  42383  cnvtrrel  42407  dfrcl2  42411  dfrcl4  42413  iunrelexp0  42439  comptiunov2i  42443  relexpaddss  42455  brtrclfv2  42464  trclfvdecomr  42465  corcltrcl  42476  cotrclrcl  42479  fsovcnvlem  42750  neicvgnvo  42852  scottabf  42985  mnuprdlem1  43017  hashnzfz  43065  lhe4.4ex1a  43074  tgqioo2  44247  sumnnodd  44333  limsup0  44397  limsup10ex  44476  liminf10ex  44477  cosnegpi  44570  itgsin0pilem1  44653  stoweidlem13  44716  wallispilem4  44771  wallispi2lem1  44774  wallispi2lem2  44775  stirlinglem3  44779  dirkertrigeqlem1  44801  fourierdlem56  44865  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fourierdlem103  44912  fourierdlem104  44913  fourierdlem112  44921  sqwvfoura  44931  fouriersw  44934  etransclem23  44960  etransclem36  44973  etransclem38  44975  carageniuncllem1  45224  0ome  45232  ovn02  45271  smflimlem4  45477  smflim  45480  smflim2  45509  smflimsup  45531  smfliminf  45534  fmtno0  46195  fmtno1  46196  fmtno2  46205  fmtno3  46206  fmtno4  46207  fmtno5lem4  46211  139prmALT  46251  31prm  46252  5tcu2e40  46270  3exp4mod41  46271  41prothprmlem2  46273  41prothprm  46274  nnsum3primesgbe  46447  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  bgoldbtbndlem1  46460  tgoldbachlt  46471  cznrnglem  46805  2t6m3t4e0  46978  zlmodzxzldeplem3  47137  ackval0  47320  ackval1  47321  ackval2  47322  ackval3  47323  ackval40  47333  ackval42  47336  ackval50  47338  disjdifb  47448  iscnrm3rlem1  47527  mndtchom  47664  sec0  47759