Theorem 3eqtri 2756

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

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

This theorem is referenced by:  csbid  3872  csbconstg  3878  csbie  3894  un23  4133  in32  4189  dfnul4  4294  unvdif  4434  undif2  4436  undifabs  4437  difun2  4440  difdifdir  4451  dfif4  4500  dfif5  4501  tpidm23  4717  dfopif  4830  dfiunv2  4994  symdif0  5044  symdifid  5046  unidif0  5310  uniop  5470  xpun  5705  dfrn2  5842  dfdmf  5850  dfrnf  5903  res0  5943  resres  5952  xpssres  5978  dfima2  6022  imai  6034  ima0  6037  imaundir  6111  xpima  6143  cnvrescnv  6156  dmresv  6161  rescnvcnv  6165  dmtpop  6179  rnsnopg  6182  resdmres  6193  resdifdi  6197  dmmpt  6201  dmco  6215  co01  6222  suc0  6397  iunsuc  6407  fresaun  6713  dffv4  6837  fvssunirnOLD  6874  f1ossf1o  7082  fpr  7108  mpo0  7454  dmoprab  7472  rnoprab  7474  elrnmpores  7507  ov6g  7533  1st0  7953  2nd0  7954  dfmpo  8058  curry1  8060  curry2  8063  fpar  8072  dftpos2  8199  tposoprab  8218  tposmpo  8219  fvmpocurryd  8227  frrlem14  8255  dfrecs3  8318  tfrlem8  8329  seqomlem3  8397  df2o3  8419  nlim2  8431  omxpenlem  9019  dfsdom2  9041  pwfir  9242  marypha2lem2  9363  sup00  9392  epinid0  9529  scottexs  9816  scott0s  9817  infxpenc2  9951  kmlem3  10082  ackbij1lem2  10149  compsscnv  10300  fin1a2lem12  10340  mulerpqlem  10884  1lt2nq  10902  axi2m1  11088  2p2e4  12292  numsuc  12639  numsucc  12665  decmul10add  12694  5p5e10  12696  6p4e10  12697  7p3e10  12700  xnegmnf  13146  pnfaddmnf  13166  fz12pr  13518  fz0tp  13565  fz0to3un2pr  13566  fz0to4untppr  13567  fz0to5un2tp  13568  fzo13pr  13686  fzo0to2pr  13687  fz01pr  13688  fzo0to3tp  13689  fzo0to42pr  13690  fzo1to4tp  13691  fldiv4p1lem1div2  13773  sq4e2t8  14140  i4  14145  crreczi  14169  fac1  14218  fac3  14221  hashkf  14273  hashinf  14276  dmhashres  14282  hashun3  14325  cshwsexaOLD  14766  dmtrclfv  14960  abs0  15227  absi  15228  trirecip  15805  geoihalfsum  15824  esum  16022  tan0  16095  coshval  16099  ef01bndlem  16128  3dvds  16277  3dvdsdec  16278  3dvds2dec  16279  sadc0  16400  3lcm2e6woprm  16561  6lcm4e12  16562  lcmf0  16580  prmo0  16983  gcdmodi  17021  karatsuba  17030  43prm  17068  139prm  17070  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  setsfun  17117  setsfun0  17118  ndxarg  17142  pmtrsn  19425  psgnprfval1  19428  sylow2a  19525  ablfac1eu  19981  sralem  21059  pzriprng1ALT  21382  opsrtoslem2  21939  ply1plusgfvi  22102  pf1rcl  22212  restcld  23035  neitr  23043  txbasval  23469  txindis  23497  cnmpt1st  23531  cnmpt2nd  23532  ufildr  23794  restmetu  24434  cphipval2  25117  reust  25257  ehl0base  25292  ismbl  25403  mbfimaopnlem  25532  itg10  25565  itg2cnlem2  25639  itgz  25658  dvmptid  25837  cos2pi  26361  tan4thpi  26399  tan4thpiOLD  26400  sincos6thpi  26401  pige3ALT  26405  dfrelog  26450  logm1  26474  dvlog  26536  efopnlem2  26542  cxpexp  26553  root1id  26640  sqrt2cxp2logb9e3  26685  ang180lem2  26696  1cubrlem  26727  quart1  26742  atandm2  26763  efiasin  26774  asinsinlem  26777  asinsin  26778  asin1  26780  acos1  26781  atancj  26796  atanlogsublem  26801  efiatan2  26803  2efiatan  26804  tanatan  26805  dvatan  26821  log2cnv  26830  log2ublem2  26833  log2ublem3  26834  birthday  26840  basellem8  26974  cht1  27051  chp1  27053  ppi1i  27054  ppi2i  27055  cht2  27058  cht3  27059  bclbnd  27167  bposlem8  27178  2lgslem3c  27285  2lgslem3d  27286  noetasuplem2  27622  noetasuplem3  27623  noetasuplem4  27624  noetainflem4  27628  bday0s  27716  old0  27743  new0  27762  left1s  27782  right1s  27783  sltlpss  27795  slelss  27796  mulsproplem13  28007  mulsproplem14  28008  precsexlem1  28085  precsexlem2  28086  onsiso  28145  bdayn0sf1o  28235  ax5seglem7  28838  axlowdimlem8  28852  axlowdimlem11  28855  vtxvalsnop  28944  iedgvalsnop  28945  umgrislfupgrlem  29025  usgrexmpledg  29165  usgredgffibi  29227  vdegp1bi  29441  edginwlk  29538  uhgrwkspthlem2  29657  clwwlkvbij  30015  wlk2v2elem2  30058  frgrwopreglem3  30216  ex-dif  30325  ex-xp  30338  ex-rn  30342  ex-lcm  30360  ex-prmo  30361  ip0i  30727  ip1ilem  30728  ipdirilem  30731  ipasslem10  30741  hvnegdii  30964  hvaddcani  30967  hvsubaddi  30968  hisubcomi  31006  normlem0  31011  normlem3  31014  normlem9  31020  bcseqi  31022  norm0  31030  norm-ii-i  31039  norm3difi  31049  normpari  31056  normpar2i  31058  polid2i  31059  shs0i  31351  chj0i  31357  pjsslem  31581  ho0subi  31697  hoaddsubi  31723  hosd1i  31724  hopncani  31726  nmop0  31888  nmfn0  31889  lnopunilem1  31912  lnophmlem2  31919  opsqrlem2  32043  pjclem1  32097  atabsi  32303  dmdbr6ati  32325  inin  32418  iuninc  32462  gtiso  32597  f1od2  32617  fpwrelmapffs  32630  fzodif1  32688  nn0split01  32715  dfdec100  32728  dp20u  32771  dp3mul10  32791  dpmul1000  32792  dpexpp1  32801  dpadd2  32803  dpmul  32806  dpmul4  32807  1mhdrd  32809  cycpmrn  33073  tocyccntz  33074  cos9thpiminplylem4  33748  cos9thpiminplylem5  33749  lmat22det  33785  ordtcnvNEW  33883  ordtrest2NEW  33886  zlmtset  33926  qqhucn  33955  esumnul  34011  mbfmcst  34223  carsggect  34282  eulerpartgbij  34336  eulerpartlemn  34345  fib0  34363  fib1  34364  fib2  34366  fib3  34367  fib4  34368  fib5  34369  fib6  34370  0rrv  34415  coinflipprob  34444  ballotlem2  34453  ballotth  34502  signsvf0  34544  itgexpif  34570  hgt750lem  34615  hgt750lem2  34616  bnj1416  35002  derang0  35129  subfac0  35137  subfac1  35138  satfv1  35323  fmla  35341  fmla0  35342  fmla0xp  35343  fmla1  35347  mthmpps  35542  problem2  35626  quad3  35630  dfrdg2  35756  pprodcnveq  35844  dffv5  35885  fullfunfv  35908  ellines  36113  rankeq1o  36132  onint1  36410  bj-xpimasn  36916  bj-pr11val  36966  bj-pr21val  36974  bj-pr22val  36980  bj-nuliotaALT  37019  bj-dfmpoa  37079  bj-opabco  37149  icorempo  37312  finxpreclem4  37355  finxp2o  37360  finxp3o  37361  matunitlindf  37585  poimirlem5  37592  poimirlem22  37609  poimirlem26  37613  poimirlem30  37617  ismblfin  37628  dvtan  37637  asindmre  37670  dvasin  37671  dvacos  37672  areacirclem5  37679  heiborlem6  37783  dmcnvep  38334  dmxrncnvep  38335  xrnres4  38364  dfcoels  38394  coss0  38443  refsymrels2  38529  dfeqvrels2  38552  refrelsredund4  38596  hdmap1cbv  41769  lcm4un  41977  lcm5un  41978  lcm6un  41979  lcm7un  41980  lcm8un  41981  3lexlogpow5ineq1  42015  5bc2eq10  42103  imaopab  42192  decpmul  42249  cxpi11d  42304  tan3rdpi  42313  sin2t3rdpi  42314  cos2t3rdpi  42315  readvrec2  42322  remul02  42366  fltnltalem  42623  sum9cubes  42633  diophrw  42720  dnwech  43010  lmhmlnmsplit  43049  fgraphopab  43165  arearect  43177  areaquad  43178  oaomoencom  43279  dmnonrel  43552  imanonrel  43555  cononrel1  43556  cononrel2  43557  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  sqrtcval  43603  resqrtvalex  43607  imsqrtvalex  43608  cnvtrrel  43632  dfrcl2  43636  dfrcl4  43638  iunrelexp0  43664  comptiunov2i  43668  relexpaddss  43680  brtrclfv2  43689  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  fsovcnvlem  43975  neicvgnvo  44077  scottabf  44202  mnuprdlem1  44234  hashnzfz  44282  lhe4.4ex1a  44291  tgqioo2  45518  sumnnodd  45601  limsup0  45665  limsup10ex  45744  liminf10ex  45745  cosnegpi  45838  itgsin0pilem1  45921  stoweidlem13  45984  wallispilem4  46039  wallispi2lem1  46042  wallispi2lem2  46043  stirlinglem3  46047  dirkertrigeqlem1  46069  fourierdlem56  46133  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  sqwvfoura  46199  fouriersw  46202  etransclem23  46228  etransclem36  46241  etransclem38  46243  carageniuncllem1  46492  0ome  46500  ovn02  46539  smflimlem4  46745  smflim  46748  smflim2  46777  smflimsup  46799  smfliminf  46802  fmtno0  47514  fmtno1  47515  fmtno2  47524  fmtno3  47525  fmtno4  47526  fmtno5lem4  47530  139prmALT  47570  31prm  47571  5tcu2e40  47589  3exp4mod41  47590  41prothprmlem2  47592  41prothprm  47593  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  bgoldbtbndlem1  47779  tgoldbachlt  47790  isuspgrim0lem  47866  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  usgrexmpl1vtx  47987  usgrexmpl1edg  47988  usgrexmpl2vtx  47992  usgrexmpl2edg  47993  gpg5gricstgr3  48054  gpgprismgr4cycllem7  48064  cznrnglem  48220  2t6m3t4e0  48309  zlmodzxzldeplem3  48464  ackval0  48642  ackval1  48643  ackval2  48644  ackval3  48645  ackval40  48655  ackval42  48658  ackval50  48660  disjdifb  48771  dftpos6  48836  tposresg  48839  tposrescnv  48840  tposres3  48842  tposid  48846  iscnrm3rlem1  48901  dfswapf2  49223  setc1onsubc  49564  sec0  49722