Theorem 3eqtri 2764

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 2760	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2760	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  csbid  3864  csbconstg  3870  csbie  3886  un23  4128  in32  4184  dfnul4  4289  unvdif  4429  undif2  4431  undifabs  4432  difun2  4435  difdifdir  4446  dfif4  4497  dfif5  4498  tpidm23  4716  dfopif  4828  dfiunv2  4991  symdif0  5042  symdifid  5044  unidif0  5307  uniop  5471  xpun  5706  dfrn2  5845  dfdmf  5853  dfrnf  5907  res0  5950  resres  5959  xpssres  5985  dfima2  6029  imai  6041  ima0  6044  imaundir  6116  xpima  6148  cnvrescnv  6161  dmresv  6166  rescnvcnv  6170  dmtpop  6184  rnsnopg  6187  resdmres  6198  resdifdi  6202  dmmpt  6206  dmco  6221  co01  6228  suc0  6402  iunsuc  6412  fresaun  6713  dffv4  6839  f1ossf1o  7083  fpr  7109  mpo0  7453  dmoprab  7471  rnoprab  7473  elrnmpores  7506  ov6g  7532  1st0  7949  2nd0  7950  dfmpo  8054  curry1  8056  curry2  8059  fpar  8068  dftpos2  8195  tposoprab  8214  tposmpo  8215  fvmpocurryd  8223  frrlem14  8251  dfrecs3  8314  tfrlem8  8325  seqomlem3  8393  df2o3  8415  nlim2  8427  omxpenlem  9018  dfsdom2  9040  pwfir  9229  marypha2lem2  9351  sup00  9380  epinid0  9520  scottexs  9811  scott0s  9812  infxpenc2  9944  kmlem3  10075  ackbij1lem2  10142  compsscnv  10293  fin1a2lem12  10333  mulerpqlem  10878  1lt2nq  10896  axi2m1  11082  2p2e4  12287  numsuc  12633  numsucc  12659  decmul10add  12688  5p5e10  12690  6p4e10  12691  7p3e10  12694  xnegmnf  13137  pnfaddmnf  13157  fz12pr  13509  fz0tp  13556  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  fzo13pr  13677  fzo0to2pr  13678  fz01pr  13679  fzo0to3tp  13680  fzo0to42pr  13681  fzo1to4tp  13682  fldiv4p1lem1div2  13767  sq4e2t8  14134  i4  14139  crreczi  14163  fac1  14212  fac3  14215  hashkf  14267  hashinf  14270  dmhashres  14276  hashun3  14319  dmtrclfv  14953  abs0  15220  absi  15221  trirecip  15798  geoihalfsum  15817  esum  16015  tan0  16088  coshval  16092  ef01bndlem  16121  3dvds  16270  3dvdsdec  16271  3dvds2dec  16272  sadc0  16393  3lcm2e6woprm  16554  6lcm4e12  16555  lcmf0  16573  prmo0  16976  gcdmodi  17014  karatsuba  17023  43prm  17061  139prm  17063  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  setsfun  17110  setsfun0  17111  ndxarg  17135  chnccat  18561  ex-chn2  18573  pmtrsn  19460  psgnprfval1  19463  sylow2a  19560  ablfac1eu  20016  sralem  21140  pzriprng1ALT  21463  opsrtoslem2  22023  ply1plusgfvi  22194  pf1rcl  22305  restcld  23128  neitr  23136  txbasval  23562  txindis  23590  cnmpt1st  23624  cnmpt2nd  23625  ufildr  23887  restmetu  24526  cphipval2  25209  reust  25349  ehl0base  25384  ismbl  25495  mbfimaopnlem  25624  itg10  25657  itg2cnlem2  25731  itgz  25750  dvmptid  25929  cos2pi  26453  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  pige3ALT  26497  dfrelog  26542  logm1  26566  dvlog  26628  efopnlem2  26634  cxpexp  26645  root1id  26732  sqrt2cxp2logb9e3  26777  ang180lem2  26788  1cubrlem  26819  quart1  26834  atandm2  26855  efiasin  26866  asinsinlem  26869  asinsin  26870  asin1  26872  acos1  26873  atancj  26888  atanlogsublem  26893  efiatan2  26895  2efiatan  26896  tanatan  26897  dvatan  26913  log2cnv  26922  log2ublem2  26925  log2ublem3  26926  birthday  26932  basellem8  27066  cht1  27143  chp1  27145  ppi1i  27146  ppi2i  27147  cht2  27150  cht3  27151  bclbnd  27259  bposlem8  27270  2lgslem3c  27377  2lgslem3d  27378  noetasuplem2  27714  noetasuplem3  27715  noetasuplem4  27716  noetainflem4  27720  bday0  27819  old0  27847  new0  27872  left1s  27903  right1s  27904  ltslpss  27916  leslss  27917  mulsproplem13  28136  mulsproplem14  28137  precsexlem1  28215  precsexlem2  28216  oniso  28279  bdayn0sf1o  28378  ax5seglem7  29020  axlowdimlem8  29034  axlowdimlem11  29037  vtxvalsnop  29126  iedgvalsnop  29127  umgrislfupgrlem  29207  usgrexmpledg  29347  usgredgffibi  29409  vdegp1bi  29623  edginwlk  29720  uhgrwkspthlem2  29839  clwwlkvbij  30200  wlk2v2elem2  30243  frgrwopreglem3  30401  ex-dif  30510  ex-xp  30523  ex-rn  30527  ex-lcm  30545  ex-prmo  30546  ip0i  30912  ip1ilem  30913  ipdirilem  30916  ipasslem10  30926  hvnegdii  31149  hvaddcani  31152  hvsubaddi  31153  hisubcomi  31191  normlem0  31196  normlem3  31199  normlem9  31205  bcseqi  31207  norm0  31215  norm-ii-i  31224  norm3difi  31234  normpari  31241  normpar2i  31243  polid2i  31244  shs0i  31536  chj0i  31542  pjsslem  31766  ho0subi  31882  hoaddsubi  31908  hosd1i  31909  hopncani  31911  nmop0  32073  nmfn0  32074  lnopunilem1  32097  lnophmlem2  32104  opsqrlem2  32228  pjclem1  32282  atabsi  32488  dmdbr6ati  32510  inin  32602  iuninc  32646  gtiso  32790  f1od2  32808  fpwrelmapffs  32823  fzodif1  32882  nn0split01  32908  dfdec100  32921  dp20u  32969  dp3mul10  32989  dpmul1000  32990  dpexpp1  32999  dpadd2  33001  dpmul  33004  dpmul4  33005  1mhdrd  33007  cycpmrn  33236  tocyccntz  33237  cos9thpiminplylem4  33962  cos9thpiminplylem5  33963  lmat22det  33999  ordtcnvNEW  34097  ordtrest2NEW  34100  zlmtset  34140  qqhucn  34169  esumnul  34225  mbfmcst  34436  carsggect  34495  eulerpartgbij  34549  eulerpartlemn  34558  fib0  34576  fib1  34577  fib2  34579  fib3  34580  fib4  34581  fib5  34582  fib6  34583  0rrv  34628  coinflipprob  34657  ballotlem2  34666  ballotth  34715  signsvf0  34757  itgexpif  34783  hgt750lem  34828  hgt750lem2  34829  bnj1416  35214  r11  35269  r12  35270  derang0  35382  subfac0  35390  subfac1  35391  satfv1  35576  fmla  35594  fmla0  35595  fmla0xp  35596  fmla1  35600  mthmpps  35795  problem2  35879  quad3  35883  dfrdg2  36006  pprodcnveq  36094  dffv5  36135  dfsuccf2  36154  fullfunfv  36160  ellines  36365  rankeq1o  36384  onint1  36662  bj-xpimasn  37200  bj-pr11val  37250  bj-pr21val  37258  bj-pr22val  37264  bj-nuliotaALT  37303  bj-dfmpoa  37368  bj-opabco  37440  icorempo  37603  finxpreclem4  37646  finxp2o  37651  finxp3o  37652  matunitlindf  37866  poimirlem5  37873  poimirlem22  37890  poimirlem26  37894  poimirlem30  37898  ismblfin  37909  dvtan  37918  asindmre  37951  dvasin  37952  dvacos  37953  areacirclem5  37960  heiborlem6  38064  dmcnvep  38636  dmxrncnvep  38637  dmcnvepres  38638  dmxrnuncnvepres  38640  xrnres4  38676  dfadjliftmap2  38705  blockadjliftmap  38706  dfblockliftmap2  38709  dfsucmap3  38711  dfsuccl2  38718  dfcoels  38768  coss0  38817  refsymrels2  38897  dfeqvrels2  38920  refrelsredund4  38964  hdmap1cbv  42175  lcm4un  42383  lcm5un  42384  lcm6un  42385  lcm7un  42386  lcm8un  42387  3lexlogpow5ineq1  42421  5bc2eq10  42509  imaopab  42600  decpmul  42655  cxpi11d  42710  tan3rdpi  42719  sin2t3rdpi  42720  cos2t3rdpi  42721  readvrec2  42728  remul02  42772  fltnltalem  43017  sum9cubes  43027  diophrw  43113  dnwech  43402  lmhmlnmsplit  43441  fgraphopab  43557  arearect  43569  areaquad  43570  oaomoencom  43671  dmnonrel  43943  imanonrel  43946  cononrel1  43947  cononrel2  43948  rclexi  43968  rtrclex  43970  dfrtrcl5  43982  sqrtcval  43994  resqrtvalex  43998  imsqrtvalex  43999  cnvtrrel  44023  dfrcl2  44027  dfrcl4  44029  iunrelexp0  44055  comptiunov2i  44059  relexpaddss  44071  brtrclfv2  44080  trclfvdecomr  44081  corcltrcl  44092  cotrclrcl  44095  fsovcnvlem  44366  neicvgnvo  44468  scottabf  44593  mnuprdlem1  44625  hashnzfz  44673  lhe4.4ex1a  44682  tgqioo2  45904  sumnnodd  45987  limsup0  46049  limsup10ex  46128  liminf10ex  46129  cosnegpi  46222  itgsin0pilem1  46305  stoweidlem13  46368  wallispilem4  46423  wallispi2lem1  46426  wallispi2lem2  46427  stirlinglem3  46431  dirkertrigeqlem1  46453  fourierdlem56  46517  fourierdlem57  46518  fourierdlem58  46519  fourierdlem62  46523  fourierdlem103  46564  fourierdlem104  46565  fourierdlem112  46573  sqwvfoura  46583  fouriersw  46586  etransclem23  46612  etransclem36  46625  etransclem38  46627  carageniuncllem1  46876  0ome  46884  ovn02  46923  smflimlem4  47129  smflim  47132  smflim2  47161  smflimsup  47183  smfliminf  47186  fmtno0  47897  fmtno1  47898  fmtno2  47907  fmtno3  47908  fmtno4  47909  fmtno5lem4  47913  139prmALT  47953  31prm  47954  5tcu2e40  47972  3exp4mod41  47973  41prothprmlem2  47975  41prothprm  47976  nnsum3primesgbe  48149  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  bgoldbtbndlem1  48162  tgoldbachlt  48173  isuspgrim0lem  48250  isubgr3stgrlem4  48326  isubgr3stgrlem6  48328  isubgr3stgrlem7  48329  usgrexmpl1vtx  48380  usgrexmpl1edg  48381  usgrexmpl2vtx  48385  usgrexmpl2edg  48386  gpg5gricstgr3  48447  gpgprismgr4cycllem7  48458  cznrnglem  48616  2t6m3t4e0  48705  zlmodzxzldeplem3  48859  ackval0  49037  ackval1  49038  ackval2  49039  ackval3  49040  ackval40  49050  ackval42  49053  ackval50  49055  disjdifb  49166  dftpos6  49231  tposresg  49234  tposrescnv  49235  tposres3  49237  tposid  49241  iscnrm3rlem1  49296  dfswapf2  49617  setc1onsubc  49958  sec0  50116