Theorem 3eqtri 2757

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 2753	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2753	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  csbid  3878  csbconstg  3884  csbie  3900  un23  4140  in32  4196  dfnul4  4301  unvdif  4441  undif2  4443  undifabs  4444  difun2  4447  difdifdir  4458  dfif4  4507  dfif5  4508  tpidm23  4724  dfopif  4837  dfiunv2  5002  symdif0  5052  symdifid  5054  unidif0  5318  uniop  5478  xpun  5715  dfrn2  5855  dfdmf  5863  dfrnf  5917  res0  5957  resres  5966  xpssres  5992  dfima2  6036  imai  6048  ima0  6051  imaundir  6126  xpima  6158  cnvrescnv  6171  dmresv  6176  rescnvcnv  6180  dmtpop  6194  rnsnopg  6197  resdmres  6208  resdifdi  6212  dmmpt  6216  dmco  6230  co01  6237  suc0  6412  iunsuc  6422  fresaun  6734  dffv4  6858  fvssunirnOLD  6895  f1ossf1o  7103  fpr  7129  mpo0  7477  dmoprab  7495  rnoprab  7497  elrnmpores  7530  ov6g  7556  1st0  7977  2nd0  7978  dfmpo  8084  curry1  8086  curry2  8089  fpar  8098  dftpos2  8225  tposoprab  8244  tposmpo  8245  fvmpocurryd  8253  frrlem14  8281  dfrecs3  8344  tfrlem8  8355  seqomlem3  8423  df2o3  8445  nlim2  8457  omxpenlem  9047  dfsdom2  9070  pwfir  9273  marypha2lem2  9394  sup00  9423  epinid0  9560  scottexs  9847  scott0s  9848  infxpenc2  9982  kmlem3  10113  ackbij1lem2  10180  compsscnv  10331  fin1a2lem12  10371  mulerpqlem  10915  1lt2nq  10933  axi2m1  11119  2p2e4  12323  numsuc  12670  numsucc  12696  decmul10add  12725  5p5e10  12727  6p4e10  12728  7p3e10  12731  xnegmnf  13177  pnfaddmnf  13197  fz12pr  13549  fz0tp  13596  fz0to3un2pr  13597  fz0to4untppr  13598  fz0to5un2tp  13599  fzo13pr  13717  fzo0to2pr  13718  fz01pr  13719  fzo0to3tp  13720  fzo0to42pr  13721  fzo1to4tp  13722  fldiv4p1lem1div2  13804  sq4e2t8  14171  i4  14176  crreczi  14200  fac1  14249  fac3  14252  hashkf  14304  hashinf  14307  dmhashres  14313  hashun3  14356  cshwsexaOLD  14797  dmtrclfv  14991  abs0  15258  absi  15259  trirecip  15836  geoihalfsum  15855  esum  16053  tan0  16126  coshval  16130  ef01bndlem  16159  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  sadc0  16431  3lcm2e6woprm  16592  6lcm4e12  16593  lcmf0  16611  prmo0  17014  gcdmodi  17052  karatsuba  17061  43prm  17099  139prm  17101  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  setsfun  17148  setsfun0  17149  ndxarg  17173  pmtrsn  19456  psgnprfval1  19459  sylow2a  19556  ablfac1eu  20012  sralem  21090  pzriprng1ALT  21413  opsrtoslem2  21970  ply1plusgfvi  22133  pf1rcl  22243  restcld  23066  neitr  23074  txbasval  23500  txindis  23528  cnmpt1st  23562  cnmpt2nd  23563  ufildr  23825  restmetu  24465  cphipval2  25148  reust  25288  ehl0base  25323  ismbl  25434  mbfimaopnlem  25563  itg10  25596  itg2cnlem2  25670  itgz  25689  dvmptid  25868  cos2pi  26392  tan4thpi  26430  tan4thpiOLD  26431  sincos6thpi  26432  pige3ALT  26436  dfrelog  26481  logm1  26505  dvlog  26567  efopnlem2  26573  cxpexp  26584  root1id  26671  sqrt2cxp2logb9e3  26716  ang180lem2  26727  1cubrlem  26758  quart1  26773  atandm2  26794  efiasin  26805  asinsinlem  26808  asinsin  26809  asin1  26811  acos1  26812  atancj  26827  atanlogsublem  26832  efiatan2  26834  2efiatan  26835  tanatan  26836  dvatan  26852  log2cnv  26861  log2ublem2  26864  log2ublem3  26865  birthday  26871  basellem8  27005  cht1  27082  chp1  27084  ppi1i  27085  ppi2i  27086  cht2  27089  cht3  27090  bclbnd  27198  bposlem8  27209  2lgslem3c  27316  2lgslem3d  27317  noetasuplem2  27653  noetasuplem3  27654  noetasuplem4  27655  noetainflem4  27659  bday0s  27747  old0  27774  new0  27793  left1s  27813  right1s  27814  sltlpss  27826  slelss  27827  mulsproplem13  28038  mulsproplem14  28039  precsexlem1  28116  precsexlem2  28117  onsiso  28176  bdayn0sf1o  28266  ax5seglem7  28869  axlowdimlem8  28883  axlowdimlem11  28886  vtxvalsnop  28975  iedgvalsnop  28976  umgrislfupgrlem  29056  usgrexmpledg  29196  usgredgffibi  29258  vdegp1bi  29472  edginwlk  29570  uhgrwkspthlem2  29691  clwwlkvbij  30049  wlk2v2elem2  30092  frgrwopreglem3  30250  ex-dif  30359  ex-xp  30372  ex-rn  30376  ex-lcm  30394  ex-prmo  30395  ip0i  30761  ip1ilem  30762  ipdirilem  30765  ipasslem10  30775  hvnegdii  30998  hvaddcani  31001  hvsubaddi  31002  hisubcomi  31040  normlem0  31045  normlem3  31048  normlem9  31054  bcseqi  31056  norm0  31064  norm-ii-i  31073  norm3difi  31083  normpari  31090  normpar2i  31092  polid2i  31093  shs0i  31385  chj0i  31391  pjsslem  31615  ho0subi  31731  hoaddsubi  31757  hosd1i  31758  hopncani  31760  nmop0  31922  nmfn0  31923  lnopunilem1  31946  lnophmlem2  31953  opsqrlem2  32077  pjclem1  32131  atabsi  32337  dmdbr6ati  32359  inin  32452  iuninc  32496  gtiso  32631  f1od2  32651  fpwrelmapffs  32664  fzodif1  32722  nn0split01  32749  dfdec100  32762  dp20u  32805  dp3mul10  32825  dpmul1000  32826  dpexpp1  32835  dpadd2  32837  dpmul  32840  dpmul4  32841  1mhdrd  32843  cycpmrn  33107  tocyccntz  33108  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  lmat22det  33819  ordtcnvNEW  33917  ordtrest2NEW  33920  zlmtset  33960  qqhucn  33989  esumnul  34045  mbfmcst  34257  carsggect  34316  eulerpartgbij  34370  eulerpartlemn  34379  fib0  34397  fib1  34398  fib2  34400  fib3  34401  fib4  34402  fib5  34403  fib6  34404  0rrv  34449  coinflipprob  34478  ballotlem2  34487  ballotth  34536  signsvf0  34578  itgexpif  34604  hgt750lem  34649  hgt750lem2  34650  bnj1416  35036  derang0  35163  subfac0  35171  subfac1  35172  satfv1  35357  fmla  35375  fmla0  35376  fmla0xp  35377  fmla1  35381  mthmpps  35576  problem2  35660  quad3  35664  dfrdg2  35790  pprodcnveq  35878  dffv5  35919  fullfunfv  35942  ellines  36147  rankeq1o  36166  onint1  36444  bj-xpimasn  36950  bj-pr11val  37000  bj-pr21val  37008  bj-pr22val  37014  bj-nuliotaALT  37053  bj-dfmpoa  37113  bj-opabco  37183  icorempo  37346  finxpreclem4  37389  finxp2o  37394  finxp3o  37395  matunitlindf  37619  poimirlem5  37626  poimirlem22  37643  poimirlem26  37647  poimirlem30  37651  ismblfin  37662  dvtan  37671  asindmre  37704  dvasin  37705  dvacos  37706  areacirclem5  37713  heiborlem6  37817  dmcnvep  38368  dmxrncnvep  38369  xrnres4  38398  dfcoels  38428  coss0  38477  refsymrels2  38563  dfeqvrels2  38586  refrelsredund4  38630  hdmap1cbv  41803  lcm4un  42011  lcm5un  42012  lcm6un  42013  lcm7un  42014  lcm8un  42015  3lexlogpow5ineq1  42049  5bc2eq10  42137  imaopab  42226  decpmul  42283  cxpi11d  42338  tan3rdpi  42347  sin2t3rdpi  42348  cos2t3rdpi  42349  readvrec2  42356  remul02  42400  fltnltalem  42657  sum9cubes  42667  diophrw  42754  dnwech  43044  lmhmlnmsplit  43083  fgraphopab  43199  arearect  43211  areaquad  43212  oaomoencom  43313  dmnonrel  43586  imanonrel  43589  cononrel1  43590  cononrel2  43591  rclexi  43611  rtrclex  43613  dfrtrcl5  43625  sqrtcval  43637  resqrtvalex  43641  imsqrtvalex  43642  cnvtrrel  43666  dfrcl2  43670  dfrcl4  43672  iunrelexp0  43698  comptiunov2i  43702  relexpaddss  43714  brtrclfv2  43723  trclfvdecomr  43724  corcltrcl  43735  cotrclrcl  43738  fsovcnvlem  44009  neicvgnvo  44111  scottabf  44236  mnuprdlem1  44268  hashnzfz  44316  lhe4.4ex1a  44325  tgqioo2  45552  sumnnodd  45635  limsup0  45699  limsup10ex  45778  liminf10ex  45779  cosnegpi  45872  itgsin0pilem1  45955  stoweidlem13  46018  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem3  46081  dirkertrigeqlem1  46103  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  sqwvfoura  46233  fouriersw  46236  etransclem23  46262  etransclem36  46275  etransclem38  46277  carageniuncllem1  46526  0ome  46534  ovn02  46573  smflimlem4  46779  smflim  46782  smflim2  46811  smflimsup  46833  smfliminf  46836  fmtno0  47545  fmtno1  47546  fmtno2  47555  fmtno3  47556  fmtno4  47557  fmtno5lem4  47561  139prmALT  47601  31prm  47602  5tcu2e40  47620  3exp4mod41  47621  41prothprmlem2  47623  41prothprm  47624  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  tgoldbachlt  47821  isuspgrim0lem  47897  isubgr3stgrlem4  47972  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  usgrexmpl1vtx  48018  usgrexmpl1edg  48019  usgrexmpl2vtx  48023  usgrexmpl2edg  48024  gpg5gricstgr3  48085  gpgprismgr4cycllem7  48095  cznrnglem  48251  2t6m3t4e0  48340  zlmodzxzldeplem3  48495  ackval0  48673  ackval1  48674  ackval2  48675  ackval3  48676  ackval40  48686  ackval42  48689  ackval50  48691  disjdifb  48802  dftpos6  48867  tposresg  48870  tposrescnv  48871  tposres3  48873  tposid  48877  iscnrm3rlem1  48932  dfswapf2  49254  setc1onsubc  49595  sec0  49753