Theorem 3eqtri 2787

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  csbid  3860  csbconstg  3866  csbie  3882  un23  4120  in32  4175  dfnul4  4281  unvdif  4429  undif2  4431  undifabs  4434  difun2  4437  difdifdir  4447  dfif4  4498  dfif5  4499  tpidm23  4718  dfopif  4830  dfiunv2  4992  symdif0  5045  symdifv  5046  symdifid  5047  unidif0  5324  unidif0OLD  5325  uniop  5492  xpun  5729  dfrn2  5872  dfdmf  5880  dfrnf  5934  res0  5976  resres  5985  xpssres  6011  dfima2  6058  imai  6070  ima0  6073  imaundir  6142  xpima  6175  cnvrescnv  6189  dmresv  6194  rescnvcnv  6200  dmtpop  6214  rnsnopg  6217  resdmres  6228  resdifdi  6232  dmmpt  6236  dmco  6251  co01  6258  relcnvtrg  6263  suc0  6435  iunsuc  6445  fresaun  6746  dffv4  6875  f1ossf1o  7122  fpr  7151  mpo0  7498  dmoprab  7516  rnoprab  7518  elrnmpores  7551  ov6g  7577  1st0  7992  2nd0  7993  dfmpo  8099  curry1  8101  curry2  8104  fpar  8113  dftpos2  8241  tposoprab  8260  tposmpo  8261  fvmpocurryd  8269  frrlem14  8298  dfrecs3  8361  tfrlem8  8373  seqomlem3  8441  df2o3  8463  nlim2  8477  omxpenlem  9076  dfsdom2  9098  pwfir  9286  marypha2lem2  9406  sup00  9435  epinid0  9577  scottabf  9878  scottexsOLD  9882  scott0bsOLD  9884  infxpenc2  10025  kmlem3  10155  ackbij1lem2  10222  compsscnv  10373  fin1a2lem12  10413  mulerpqlem  10964  1lt2nq  10982  axi2m1  11168  2p2e4  12399  numsuc  12750  numsucc  12781  decmul10add  12810  5p5e10  12812  6p4e10  12813  7p3e10  12816  xnegmnf  13262  pnfaddmnf  13282  fz12pr  13636  fz0tp  13683  fz0to3un2pr  13684  fz0to4untppr  13685  fz0to5un2tp  13686  fzo13pr  13805  fzo0to2pr  13806  fz01pr  13807  fzo0to3tp  13808  fzo0to42pr  13809  fzo1to4tp  13810  fldiv4p1lem1div2  13896  sq4e2t8  14263  i4  14268  crreczi  14292  fac1  14341  fac3  14344  hashkf  14396  hashinf  14399  dmhashres  14405  hashun3  14448  dmtrclfv  15091  abs0  15372  absi  15373  trirecip  15952  geoihalfsum  15971  esum  16166  tan0  16239  coshval  16243  ef01bndlem  16272  3dvds  16421  3dvdsdec  16422  3dvds2dec  16423  sadc0  16544  3lcm2e6woprm  16705  6lcm4e12  16706  lcmf0  16724  prmo0  17128  prmo3  17133  gcdmodi  17166  karatsuba  17175  43prm  17214  139prm  17216  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  2503lem1  17229  2503lem2  17230  2503lem3  17231  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  setsfun  17263  setsfun0  17264  ndxarg  17288  chnccat  18714  ex-chn2  18726  pmtrsn  19646  psgnprfval1  19649  sylow2a  19746  ablfac1eu  20202  sralem  21360  pzriprng1ALT  21709  opsrtoslem2  22272  ply1plusgfvi  22466  pf1rcl  22574  matunitlindf  22903  restcld  23397  neitr  23405  txbasval  23832  txindis  23860  cnmpt1st  23894  cnmpt2nd  23895  ufildr  24157  restmetu  24796  cphipval2  25469  reust  25609  ehl0base  25644  ismbl  25754  mbfimaopnlem  25883  itg10  25916  itg2cnlem2  25990  itgz  26008  dvmptid  26184  cos2pi  26714  tan4thpi  26752  sincos6thpi  26753  pige3ALT  26757  dfrelog  26802  logm1  26826  dvlog  26888  efopnlem2  26894  cxpexp  26905  root1id  26991  sqrt2cxp2logb9e3  27036  ang180lem2  27047  1cubrlem  27078  quart1  27093  atandm2  27114  efiasin  27125  asinsinlem  27128  asinsin  27129  asin1  27131  acos1  27132  atancj  27147  atanlogsublem  27152  efiatan2  27154  2efiatan  27155  tanatan  27156  dvatan  27172  log2cnv  27181  log2ublem2  27184  log2ublem3  27185  birthday  27191  cht1  27401  chp1  27403  ppi1i  27404  ppi2i  27405  cht2  27408  cht3  27409  bclbnd  27516  bposlem8  27527  2lgslem3c  27634  2lgslem3d  27635  noetasuplem2  27970  noetasuplem3  27971  noetasuplem4  27972  noetainflem4  27976  bday0  28076  old0  28104  new0  28129  left1s  28160  right1s  28161  ltslpss  28173  leslss  28174  mulsproplem13  28393  mulsproplem14  28394  precsexlem1  28472  precsexlem2  28473  oniso  28536  bdayn0sf1o  28635  ax5seglem7  29392  axlowdimlem8  29406  axlowdimlem11  29409  vtxvalsnop  29498  iedgvalsnop  29499  umgrislfupgrlem  29579  usgrexmpledg  29722  usgredgffibi  29784  vdegp1bi  29997  edginwlk  30094  uhgrwkspthlem2  30219  clwwlkvbij  30583  wlk2v2elem2  30636  frgrwopreglem3  30794  ex-dif  30903  ex-xp  30916  ex-rn  30920  ex-lcm  30938  ex-prmo  30939  ip0i  31306  ip1ilem  31307  ipdirilem  31310  ipasslem10  31320  hvnegdii  31543  hvaddcani  31546  hvsubaddi  31547  hisubcomi  31585  normlem0  31590  normlem3  31593  normlem9  31599  bcseqi  31601  norm0  31609  norm-ii-i  31618  norm3difi  31628  normpari  31635  normpar2i  31637  polid2i  31638  shs0i  31930  chj0i  31936  pjsslem  32160  ho0subi  32276  hoaddsubi  32302  hosd1i  32303  hopncani  32305  nmop0  32467  nmfn0  32468  lnopunilem1  32491  lnophmlem2  32498  opsqrlem2  32622  pjclem1  32676  atabsi  32882  dmdbr6ati  32904  inin  32991  iuninc  33034  gtiso  33173  f1od2  33190  fpwrelmapffs  33205  fzodif1  33263  nn0split01  33288  dfdec100  33300  dp20u  33323  dp3mul10  33343  dpmul1000  33344  dpexpp1  33353  dpadd2  33355  dpmul  33358  dpmul4  33359  1mhdrd  33361  cycpmrn  33583  tocyccntz  33584  cos9thpiminplylem4  34295  cos9thpiminplylem5  34296  lmat22det  34332  ordtcnvNEW  34430  ordtrest2NEW  34433  zlmtset  34473  qqhucn  34502  esumnul  34558  mbfmcst  34770  carsggect  34829  eulerpartgbij  34883  eulerpartlemn  34892  fib0  34910  fib1  34911  fib2  34913  fib3  34914  fib4  34915  fib5  34916  fib6  34917  0rrv  34962  coinflipprob  34991  ballotlem2  35000  ballotth  35049  signsvf0  35088  itgexpif  35114  hgt750lem  35159  hgt750lem2  35160  bnj1416  35548  r11  35601  r12  35602  derang0  35748  subfac0  35756  subfac1  35757  satfv1  35942  fmla  35960  fmla0  35961  fmla0xp  35962  fmla1  35966  mthmpps  36161  problem2  36245  quad3  36249  dfrdg2  36372  pprodcnveq  36460  dffv5  36501  dfsuccf2  36520  fullfunfv  36526  ellines  36732  rankeq1o  36751  onint1  37068  bj-xpimasn  37699  bj-pr11val  37749  bj-pr21val  37757  bj-pr22val  37763  bj-nuliotaALT  37802  bj-dfmpoa  37868  bj-opabco  37940  icorempo  38105  finxpreclem4  38148  finxp2o  38153  finxp3o  38154  poimirlem5  38374  poimirlem22  38391  poimirlem26  38395  poimirlem30  38399  ismblfin  38410  dvtan  38419  asindmre  38452  dvasin  38453  dvacos  38454  areacirclem5  38461  heiborlem6  38566  dmcnvep  39136  dmxrncnvep  39137  dmcnvepres  39138  dmxrnuncnvepres  39140  xrnres4  39176  dfadjliftmap2  39205  blockadjliftmap  39206  dfblockliftmap2  39209  dfsucmap3  39211  dfsuccl2  39218  dfcoels  39268  coss0  39317  refsymrels2  39397  dfeqvrels2  39420  refrelsredund4  39464  hdmap1cbv  42675  lcm4un  42882  lcm5un  42883  lcm6un  42884  lcm7un  42885  lcm8un  42886  3lexlogpow5ineq1  42920  5bc2eq10  43008  imaopab  43101  decpmul  43163  cxpi11d  43218  tan3rdpi  43227  sin2t3rdpi  43228  cos2t3rdpi  43229  readvrec2  43236  remul02  43280  fltnltalem  43508  sum9cubes  43518  diophrw  43604  dnwech  43889  lmhmlnmsplit  43928  fgraphopab  44044  arearect  44056  areaquad  44057  oaomoencom  44158  dmnonrel  44430  imanonrel  44433  cononrel1  44434  cononrel2  44435  rclexi  44455  rtrclex  44457  dfrtrcl5  44469  sqrtcval  44481  resqrtvalex  44485  imsqrtvalex  44486  cnvtrrel  44510  dfrcl2  44514  dfrcl4  44516  iunrelexp0  44542  comptiunov2i  44546  relexpaddss  44558  brtrclfv2  44567  trclfvdecomr  44568  corcltrcl  44579  cotrclrcl  44582  fsovcnvlem  44853  neicvgnvo  44955  mnuprdlem1  45096  hashnzfz  45144  lhe4.4ex1a  45153  tgqioo2  46377  sumnnodd  46460  limsup0  46522  limsup10ex  46601  liminf10ex  46602  cosnegpi  46695  itgsin0pilem1  46778  stoweidlem13  46841  wallispilem4  46896  wallispi2lem1  46899  wallispi2lem2  46900  stirlinglem3  46904  dirkertrigeqlem1  46926  fourierdlem56  46990  fourierdlem57  46991  fourierdlem58  46992  fourierdlem62  46996  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  sqwvfoura  47056  fouriersw  47059  etransclem23  47085  etransclem36  47098  etransclem38  47100  carageniuncllem1  47349  0ome  47357  ovn02  47396  smflimlem4  47602  smflim  47605  smflim2  47634  smflimsup  47656  smfliminf  47659  numtowerdt  47734  cos5t  47743  goldpolyfactor  47745  goldratmolem2  47751  goldratval  47754  cjnpoly  47757  fmtno0  48443  fmtno1  48444  fmtno2  48453  fmtno3  48454  fmtno4  48455  fmtno5lem4  48459  139prmALT  48499  31prm  48500  5tcu2e40  48518  3exp4mod41  48519  41prothprmlem2  48521  41prothprm  48522  ppivalnn4  48530  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbndlem1  48721  tgoldbachlt  48732  isuspgrim0lem  48809  isubgr3stgrlem4  48885  isubgr3stgrlem6  48887  isubgr3stgrlem7  48888  usgrexmpl1vtx  48939  usgrexmpl1edg  48940  usgrexmpl2vtx  48944  usgrexmpl2edg  48945  gpg5gricstgr3  49006  gpgprismgr4cycllem7  49017  cznrnglem  49174  2t6m3t4e0  49278  zlmodzxzldeplem3  49432  ackval0  49610  ackval1  49611  ackval2  49612  ackval3  49613  ackval40  49623  ackval42  49626  ackval50  49628  disjdifb  49738  dftpos6  49801  tposresg  49804  tposrescnv  49805  tposres3  49807  tposid  49811  iscnrm3rlem1  49866  dfswapf2  50187  setc1onsubc  50528  sec0  50686  dvcsc  50690  dvcot  50691