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 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  csbid  3902  csbconstg  3908  csbie  3925  un23  4166  in32  4220  dfnul4  4324  dfnul2OLD  4327  unvdif  4476  undif2  4478  undifabs  4479  difun2  4482  difdifdir  4493  dfif4  4545  dfif5  4546  tpidm23  4763  dfopif  4872  dfiunv2  5039  symdif0  5089  symdifid  5091  unidif0  5360  uniop  5517  xpun  5751  dfrn2  5891  dfdmf  5899  dfrnf  5952  res0  5989  resres  5998  xpssres  6023  dfima2  6066  imai  6078  ima0  6081  imaundir  6157  xpima  6188  cnvrescnv  6201  dmresv  6206  rescnvcnv  6210  dmtpop  6224  rnsnopg  6227  resdmres  6238  resdifdi  6242  dmmpt  6246  dmco  6260  co01  6267  suc0  6446  iunsuc  6456  fresaun  6768  dffv4  6893  fvssunirnOLD  6930  f1ossf1o  7137  fpr  7163  mpo0  7505  dmoprab  7522  rnoprab  7524  elrnmpores  7559  ov6g  7585  1st0  8000  2nd0  8001  dfmpo  8107  curry1  8109  curry2  8112  fpar  8121  dftpos2  8249  tposoprab  8268  tposmpo  8269  fvmpocurryd  8277  frrlem14  8305  dfwrecsOLD  8319  wfrlem14OLD  8343  wfrlem16OLD  8345  dfrecs3  8393  dfrecs3OLD  8394  tfrlem8  8405  seqomlem3  8473  df2o3  8495  nlim2  8511  omxpenlem  9098  dfsdom2  9121  pwfir  9201  marypha2lem2  9461  sup00  9489  epinid0  9625  scottexs  9912  scott0s  9913  infxpenc2  10047  kmlem3  10177  ackbij1lem2  10246  compsscnv  10396  fin1a2lem12  10436  mulerpqlem  10980  1lt2nq  10998  axi2m1  11184  2p2e4  12380  numsuc  12724  numsucc  12750  decmul10add  12779  5p5e10  12781  6p4e10  12782  7p3e10  12785  xnegmnf  13224  pnfaddmnf  13244  fz12pr  13593  fz0tp  13637  fz0to3un2pr  13638  fzo13pr  13751  fzo0to2pr  13752  fzo0to3tp  13753  fzo0to42pr  13754  fzo1to4tp  13755  fldiv4p1lem1div2  13836  sq4e2t8  14198  i4  14203  crreczi  14226  fac1  14272  fac3  14275  hashkf  14327  hashinf  14330  dmhashres  14336  hashun3  14379  cshwsexaOLD  14811  dmtrclfv  15001  abs0  15268  absi  15269  trirecip  15845  geoihalfsum  15864  esum  16060  tan0  16131  coshval  16135  ef01bndlem  16164  3dvds  16311  3dvdsdec  16312  3dvds2dec  16313  sadc0  16432  3lcm2e6woprm  16589  6lcm4e12  16590  lcmf0  16608  prmo0  17008  gcdmodi  17046  karatsuba  17056  43prm  17094  139prm  17096  631prm  17099  1259lem1  17103  1259lem2  17104  1259lem3  17105  1259lem4  17106  1259lem5  17107  2503lem1  17109  2503lem2  17110  2503lem3  17111  4001lem1  17113  4001lem2  17114  4001lem3  17115  4001lem4  17116  setsfun  17143  setsfun0  17144  ndxarg  17168  pmtrsn  19486  psgnprfval1  19489  sylow2a  19586  ablfac1eu  20042  sralem  21073  sralemOLD  21074  pzriprng1ALT  21439  opsrtoslem2  22022  ply1plusgfvi  22184  pf1rcl  22293  restcld  23120  neitr  23128  txbasval  23554  txindis  23582  cnmpt1st  23616  cnmpt2nd  23617  ufildr  23879  restmetu  24523  cphipval2  25213  reust  25353  ehl0base  25388  ismbl  25499  mbfimaopnlem  25628  itg10  25661  itg2cnlem2  25736  itgz  25754  dvmptid  25933  cos2pi  26456  tan4thpi  26494  sincos6thpi  26495  pige3ALT  26499  dfrelog  26544  logm1  26568  dvlog  26630  efopnlem2  26636  cxpexp  26647  root1id  26734  sqrt2cxp2logb9e3  26776  ang180lem2  26787  1cubrlem  26818  quart1  26833  atandm2  26854  efiasin  26865  asinsinlem  26868  asinsin  26869  asin1  26871  acos1  26872  atancj  26887  atanlogsublem  26892  efiatan2  26894  2efiatan  26895  tanatan  26896  dvatan  26912  log2cnv  26921  log2ublem2  26924  log2ublem3  26925  birthday  26931  basellem8  27065  cht1  27142  chp1  27144  ppi1i  27145  ppi2i  27146  cht2  27149  cht3  27150  bclbnd  27258  bposlem8  27269  2lgslem3c  27376  2lgslem3d  27377  noetasuplem2  27713  noetasuplem3  27714  noetasuplem4  27715  noetainflem4  27719  bday0s  27807  old0  27832  new0  27847  left1s  27867  right1s  27868  sltlpss  27879  slelss  27880  mulsproplem13  28078  mulsproplem14  28079  precsexlem1  28155  precsexlem2  28156  ax5seglem7  28818  axlowdimlem8  28832  axlowdimlem11  28835  vtxvalsnop  28926  iedgvalsnop  28927  umgrislfupgrlem  29007  usgrexmpledg  29147  usgredgffibi  29209  vdegp1bi  29423  edginwlk  29521  uhgrwkspthlem2  29640  clwwlkvbij  29995  wlk2v2elem2  30038  frgrwopreglem3  30196  ex-dif  30305  ex-xp  30318  ex-rn  30322  ex-lcm  30340  ex-prmo  30341  ip0i  30707  ip1ilem  30708  ipdirilem  30711  ipasslem10  30721  hvnegdii  30944  hvaddcani  30947  hvsubaddi  30948  hisubcomi  30986  normlem0  30991  normlem3  30994  normlem9  31000  bcseqi  31002  norm0  31010  norm-ii-i  31019  norm3difi  31029  normpari  31036  normpar2i  31038  polid2i  31039  shs0i  31331  chj0i  31337  pjsslem  31561  ho0subi  31677  hoaddsubi  31703  hosd1i  31704  hopncani  31706  nmop0  31868  nmfn0  31869  lnopunilem1  31892  lnophmlem2  31899  opsqrlem2  32023  pjclem1  32077  atabsi  32283  dmdbr6ati  32305  inin  32390  iuninc  32430  gtiso  32562  f1od2  32585  fpwrelmapffs  32598  fzodif1  32643  nn0split01  32665  dfdec100  32678  dp20u  32686  dp3mul10  32706  dpmul1000  32707  dpexpp1  32716  dpadd2  32718  dpmul  32721  dpmul4  32722  1mhdrd  32724  cycpmrn  32956  tocyccntz  32957  lmat22det  33554  ordtcnvNEW  33652  ordtrest2NEW  33655  zlmtset  33696  zlmtsetOLD  33697  qqhucn  33724  esumnul  33798  mbfmcst  34010  carsggect  34069  eulerpartgbij  34123  eulerpartlemn  34132  fib0  34150  fib1  34151  fib2  34153  fib3  34154  fib4  34155  fib5  34156  fib6  34157  0rrv  34202  coinflipprob  34230  ballotlem2  34239  ballotth  34288  signsvf0  34343  itgexpif  34369  hgt750lem  34414  hgt750lem2  34415  bnj1416  34801  derang0  34910  subfac0  34918  subfac1  34919  satfv1  35104  fmla  35122  fmla0  35123  fmla0xp  35124  fmla1  35128  mthmpps  35323  problem2  35401  quad3  35405  dfrdg2  35522  pprodcnveq  35610  dffv5  35651  fullfunfv  35674  ellines  35879  rankeq1o  35898  onint1  36064  bj-xpimasn  36565  bj-pr11val  36615  bj-pr21val  36623  bj-pr22val  36629  bj-nuliotaALT  36668  bj-dfmpoa  36728  bj-opabco  36798  icorempo  36961  finxpreclem4  37004  finxp2o  37009  finxp3o  37010  matunitlindf  37222  poimirlem5  37229  poimirlem22  37246  poimirlem26  37250  poimirlem30  37254  ismblfin  37265  dvtan  37274  asindmre  37307  dvasin  37308  dvacos  37309  areacirclem5  37316  heiborlem6  37420  xrnres4  38007  dfcoels  38032  coss0  38081  refsymrels2  38167  dfeqvrels2  38190  refrelsredund4  38234  hdmap1cbv  41405  lcm4un  41619  lcm5un  41620  lcm6un  41621  lcm7un  41622  lcm8un  41623  3lexlogpow5ineq1  41657  5bc2eq10  41745  2xp3dxp2ge1d  41827  imaopab  41853  decpmul  41997  cxpi11d  42049  remul02  42095  fltnltalem  42221  sum9cubes  42231  diophrw  42321  dnwech  42614  lmhmlnmsplit  42653  fgraphopab  42773  arearect  42785  areaquad  42786  oaomoencom  42888  dmnonrel  43162  imanonrel  43165  cononrel1  43166  cononrel2  43167  rclexi  43187  rtrclex  43189  dfrtrcl5  43201  sqrtcval  43213  resqrtvalex  43217  imsqrtvalex  43218  cnvtrrel  43242  dfrcl2  43246  dfrcl4  43248  iunrelexp0  43274  comptiunov2i  43278  relexpaddss  43290  brtrclfv2  43299  trclfvdecomr  43300  corcltrcl  43311  cotrclrcl  43314  fsovcnvlem  43585  neicvgnvo  43687  scottabf  43819  mnuprdlem1  43851  hashnzfz  43899  lhe4.4ex1a  43908  tgqioo2  45070  sumnnodd  45156  limsup0  45220  limsup10ex  45299  liminf10ex  45300  cosnegpi  45393  itgsin0pilem1  45476  stoweidlem13  45539  wallispilem4  45594  wallispi2lem1  45597  wallispi2lem2  45598  stirlinglem3  45602  dirkertrigeqlem1  45624  fourierdlem56  45688  fourierdlem57  45689  fourierdlem58  45690  fourierdlem62  45694  fourierdlem103  45735  fourierdlem104  45736  fourierdlem112  45744  sqwvfoura  45754  fouriersw  45757  etransclem23  45783  etransclem36  45796  etransclem38  45798  carageniuncllem1  46047  0ome  46055  ovn02  46094  smflimlem4  46300  smflim  46303  smflim2  46332  smflimsup  46354  smfliminf  46357  fmtno0  47017  fmtno1  47018  fmtno2  47027  fmtno3  47028  fmtno4  47029  fmtno5lem4  47033  139prmALT  47073  31prm  47074  5tcu2e40  47092  3exp4mod41  47093  41prothprmlem2  47095  41prothprm  47096  nnsum3primesgbe  47269  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  bgoldbtbndlem1  47282  tgoldbachlt  47293  isuspgrim0lem  47355  cznrnglem  47507  2t6m3t4e0  47598  zlmodzxzldeplem3  47756  ackval0  47939  ackval1  47940  ackval2  47941  ackval3  47942  ackval40  47952  ackval42  47955  ackval50  47957  disjdifb  48066  iscnrm3rlem1  48145  mndtchom  48282  sec0  48377