Theorem 3eqtri 2762

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

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

This theorem is referenced by:  csbid  3887  csbconstg  3893  csbie  3909  un23  4149  in32  4205  dfnul4  4310  unvdif  4450  undif2  4452  undifabs  4453  difun2  4456  difdifdir  4467  dfif4  4516  dfif5  4517  tpidm23  4733  dfopif  4846  dfiunv2  5011  symdif0  5061  symdifid  5063  unidif0  5330  uniop  5490  xpun  5728  dfrn2  5868  dfdmf  5876  dfrnf  5930  res0  5970  resres  5979  xpssres  6005  dfima2  6049  imai  6061  ima0  6064  imaundir  6139  xpima  6171  cnvrescnv  6184  dmresv  6189  rescnvcnv  6193  dmtpop  6207  rnsnopg  6210  resdmres  6221  resdifdi  6225  dmmpt  6229  dmco  6243  co01  6250  suc0  6428  iunsuc  6438  fresaun  6748  dffv4  6872  fvssunirnOLD  6909  f1ossf1o  7117  fpr  7143  mpo0  7490  dmoprab  7508  rnoprab  7510  elrnmpores  7543  ov6g  7569  1st0  7992  2nd0  7993  dfmpo  8099  curry1  8101  curry2  8104  fpar  8113  dftpos2  8240  tposoprab  8259  tposmpo  8260  fvmpocurryd  8268  frrlem14  8296  dfwrecsOLD  8310  wfrlem14OLD  8334  wfrlem16OLD  8336  dfrecs3  8384  dfrecs3OLD  8385  tfrlem8  8396  seqomlem3  8464  df2o3  8486  nlim2  8500  omxpenlem  9085  dfsdom2  9108  pwfir  9325  marypha2lem2  9446  sup00  9475  epinid0  9612  scottexs  9899  scott0s  9900  infxpenc2  10034  kmlem3  10165  ackbij1lem2  10232  compsscnv  10383  fin1a2lem12  10423  mulerpqlem  10967  1lt2nq  10985  axi2m1  11171  2p2e4  12373  numsuc  12720  numsucc  12746  decmul10add  12775  5p5e10  12777  6p4e10  12778  7p3e10  12781  xnegmnf  13224  pnfaddmnf  13244  fz12pr  13596  fz0tp  13643  fz0to3un2pr  13644  fz0to4untppr  13645  fz0to5un2tp  13646  fzo13pr  13763  fzo0to2pr  13764  fz01pr  13765  fzo0to3tp  13766  fzo0to42pr  13767  fzo1to4tp  13768  fldiv4p1lem1div2  13850  sq4e2t8  14215  i4  14220  crreczi  14244  fac1  14293  fac3  14296  hashkf  14348  hashinf  14351  dmhashres  14357  hashun3  14400  cshwsexaOLD  14841  dmtrclfv  15035  abs0  15302  absi  15303  trirecip  15877  geoihalfsum  15896  esum  16094  tan0  16167  coshval  16171  ef01bndlem  16200  3dvds  16348  3dvdsdec  16349  3dvds2dec  16350  sadc0  16471  3lcm2e6woprm  16632  6lcm4e12  16633  lcmf0  16651  prmo0  17054  gcdmodi  17092  karatsuba  17101  43prm  17139  139prm  17141  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503lem3  17156  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  setsfun  17188  setsfun0  17189  ndxarg  17213  pmtrsn  19498  psgnprfval1  19501  sylow2a  19598  ablfac1eu  20054  sralem  21132  pzriprng1ALT  21455  opsrtoslem2  22012  ply1plusgfvi  22175  pf1rcl  22285  restcld  23108  neitr  23116  txbasval  23542  txindis  23570  cnmpt1st  23604  cnmpt2nd  23605  ufildr  23867  restmetu  24507  cphipval2  25191  reust  25331  ehl0base  25366  ismbl  25477  mbfimaopnlem  25606  itg10  25639  itg2cnlem2  25713  itgz  25732  dvmptid  25911  cos2pi  26435  tan4thpi  26473  tan4thpiOLD  26474  sincos6thpi  26475  pige3ALT  26479  dfrelog  26524  logm1  26548  dvlog  26610  efopnlem2  26616  cxpexp  26627  root1id  26714  sqrt2cxp2logb9e3  26759  ang180lem2  26770  1cubrlem  26801  quart1  26816  atandm2  26837  efiasin  26848  asinsinlem  26851  asinsin  26852  asin1  26854  acos1  26855  atancj  26870  atanlogsublem  26875  efiatan2  26877  2efiatan  26878  tanatan  26879  dvatan  26895  log2cnv  26904  log2ublem2  26907  log2ublem3  26908  birthday  26914  basellem8  27048  cht1  27125  chp1  27127  ppi1i  27128  ppi2i  27129  cht2  27132  cht3  27133  bclbnd  27241  bposlem8  27252  2lgslem3c  27359  2lgslem3d  27360  noetasuplem2  27696  noetasuplem3  27697  noetasuplem4  27698  noetainflem4  27702  bday0s  27790  old0  27815  new0  27830  left1s  27850  right1s  27851  sltlpss  27862  slelss  27863  mulsproplem13  28071  mulsproplem14  28072  precsexlem1  28148  precsexlem2  28149  ax5seglem7  28860  axlowdimlem8  28874  axlowdimlem11  28877  vtxvalsnop  28966  iedgvalsnop  28967  umgrislfupgrlem  29047  usgrexmpledg  29187  usgredgffibi  29249  vdegp1bi  29463  edginwlk  29561  uhgrwkspthlem2  29682  clwwlkvbij  30040  wlk2v2elem2  30083  frgrwopreglem3  30241  ex-dif  30350  ex-xp  30363  ex-rn  30367  ex-lcm  30385  ex-prmo  30386  ip0i  30752  ip1ilem  30753  ipdirilem  30756  ipasslem10  30766  hvnegdii  30989  hvaddcani  30992  hvsubaddi  30993  hisubcomi  31031  normlem0  31036  normlem3  31039  normlem9  31045  bcseqi  31047  norm0  31055  norm-ii-i  31064  norm3difi  31074  normpari  31081  normpar2i  31083  polid2i  31084  shs0i  31376  chj0i  31382  pjsslem  31606  ho0subi  31722  hoaddsubi  31748  hosd1i  31749  hopncani  31751  nmop0  31913  nmfn0  31914  lnopunilem1  31937  lnophmlem2  31944  opsqrlem2  32068  pjclem1  32122  atabsi  32328  dmdbr6ati  32350  inin  32443  iuninc  32487  gtiso  32624  f1od2  32644  fpwrelmapffs  32657  fzodif1  32715  nn0split01  32742  dfdec100  32755  dp20u  32798  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpmul  32833  dpmul4  32834  1mhdrd  32836  cycpmrn  33100  tocyccntz  33101  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  lmat22det  33799  ordtcnvNEW  33897  ordtrest2NEW  33900  zlmtset  33940  qqhucn  33969  esumnul  34025  mbfmcst  34237  carsggect  34296  eulerpartgbij  34350  eulerpartlemn  34359  fib0  34377  fib1  34378  fib2  34380  fib3  34381  fib4  34382  fib5  34383  fib6  34384  0rrv  34429  coinflipprob  34458  ballotlem2  34467  ballotth  34516  signsvf0  34558  itgexpif  34584  hgt750lem  34629  hgt750lem2  34630  bnj1416  35016  derang0  35137  subfac0  35145  subfac1  35146  satfv1  35331  fmla  35349  fmla0  35350  fmla0xp  35351  fmla1  35355  mthmpps  35550  problem2  35634  quad3  35638  dfrdg2  35759  pprodcnveq  35847  dffv5  35888  fullfunfv  35911  ellines  36116  rankeq1o  36135  onint1  36413  bj-xpimasn  36919  bj-pr11val  36969  bj-pr21val  36977  bj-pr22val  36983  bj-nuliotaALT  37022  bj-dfmpoa  37082  bj-opabco  37152  icorempo  37315  finxpreclem4  37358  finxp2o  37363  finxp3o  37364  matunitlindf  37588  poimirlem5  37595  poimirlem22  37612  poimirlem26  37616  poimirlem30  37620  ismblfin  37631  dvtan  37640  asindmre  37673  dvasin  37674  dvacos  37675  areacirclem5  37682  heiborlem6  37786  xrnres4  38369  dfcoels  38394  coss0  38443  refsymrels2  38529  dfeqvrels2  38552  refrelsredund4  38596  hdmap1cbv  41767  lcm4un  41975  lcm5un  41976  lcm6un  41977  lcm7un  41978  lcm8un  41979  3lexlogpow5ineq1  42013  5bc2eq10  42101  2xp3dxp2ge1d  42200  imaopab  42228  decpmul  42285  cxpi11d  42339  tan3rdpi  42346  readvrec2  42351  remul02  42395  fltnltalem  42632  sum9cubes  42642  diophrw  42729  dnwech  43019  lmhmlnmsplit  43058  fgraphopab  43174  arearect  43186  areaquad  43187  oaomoencom  43288  dmnonrel  43561  imanonrel  43564  cononrel1  43565  cononrel2  43566  rclexi  43586  rtrclex  43588  dfrtrcl5  43600  sqrtcval  43612  resqrtvalex  43616  imsqrtvalex  43617  cnvtrrel  43641  dfrcl2  43645  dfrcl4  43647  iunrelexp0  43673  comptiunov2i  43677  relexpaddss  43689  brtrclfv2  43698  trclfvdecomr  43699  corcltrcl  43710  cotrclrcl  43713  fsovcnvlem  43984  neicvgnvo  44086  scottabf  44212  mnuprdlem1  44244  hashnzfz  44292  lhe4.4ex1a  44301  tgqioo2  45524  sumnnodd  45607  limsup0  45671  limsup10ex  45750  liminf10ex  45751  cosnegpi  45844  itgsin0pilem1  45927  stoweidlem13  45990  wallispilem4  46045  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem3  46053  dirkertrigeqlem1  46075  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  sqwvfoura  46205  fouriersw  46208  etransclem23  46234  etransclem36  46247  etransclem38  46249  carageniuncllem1  46498  0ome  46506  ovn02  46545  smflimlem4  46751  smflim  46754  smflim2  46783  smflimsup  46805  smfliminf  46808  fmtno0  47502  fmtno1  47503  fmtno2  47512  fmtno3  47513  fmtno4  47514  fmtno5lem4  47518  139prmALT  47558  31prm  47559  5tcu2e40  47577  3exp4mod41  47578  41prothprmlem2  47580  41prothprm  47581  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem1  47767  tgoldbachlt  47778  isuspgrim0lem  47854  isubgr3stgrlem4  47929  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  usgrexmpl1vtx  47975  usgrexmpl1edg  47976  usgrexmpl2vtx  47980  usgrexmpl2edg  47981  gpg5gricstgr3  48040  gpgprismgr4cycllem7  48048  cznrnglem  48182  2t6m3t4e0  48271  zlmodzxzldeplem3  48426  ackval0  48608  ackval1  48609  ackval2  48610  ackval3  48611  ackval40  48621  ackval42  48624  ackval50  48626  disjdifb  48736  dftpos6  48798  tposresg  48801  tposrescnv  48802  tposres3  48804  tposid  48808  iscnrm3rlem1  48862  dfswapf2  49126  setc1onsubc  49427  sec0  49572