Theorem 3eqtri 2758

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  csbid  3858  csbconstg  3864  csbie  3880  un23  4119  in32  4175  dfnul4  4280  unvdif  4420  undif2  4422  undifabs  4423  difun2  4426  difdifdir  4437  dfif4  4486  dfif5  4487  tpidm23  4705  dfopif  4817  dfiunv2  4979  symdif0  5028  symdifid  5030  unidif0  5293  uniop  5450  xpun  5685  dfrn2  5823  dfdmf  5831  dfrnf  5885  res0  5927  resres  5936  xpssres  5962  dfima2  6006  imai  6018  ima0  6021  imaundir  6092  xpima  6124  cnvrescnv  6137  dmresv  6142  rescnvcnv  6146  dmtpop  6160  rnsnopg  6163  resdmres  6174  resdifdi  6178  dmmpt  6182  dmco  6197  co01  6204  suc0  6378  iunsuc  6388  fresaun  6689  dffv4  6814  f1ossf1o  7056  fpr  7082  mpo0  7426  dmoprab  7444  rnoprab  7446  elrnmpores  7479  ov6g  7505  1st0  7922  2nd0  7923  dfmpo  8027  curry1  8029  curry2  8032  fpar  8041  dftpos2  8168  tposoprab  8187  tposmpo  8188  fvmpocurryd  8196  frrlem14  8224  dfrecs3  8287  tfrlem8  8298  seqomlem3  8366  df2o3  8388  nlim2  8400  omxpenlem  8986  dfsdom2  9008  pwfir  9196  marypha2lem2  9315  sup00  9344  epinid0  9484  scottexs  9775  scott0s  9776  infxpenc2  9908  kmlem3  10039  ackbij1lem2  10106  compsscnv  10257  fin1a2lem12  10297  mulerpqlem  10841  1lt2nq  10859  axi2m1  11045  2p2e4  12250  numsuc  12597  numsucc  12623  decmul10add  12652  5p5e10  12654  6p4e10  12655  7p3e10  12658  xnegmnf  13104  pnfaddmnf  13124  fz12pr  13476  fz0tp  13523  fz0to3un2pr  13524  fz0to4untppr  13525  fz0to5un2tp  13526  fzo13pr  13644  fzo0to2pr  13645  fz01pr  13646  fzo0to3tp  13647  fzo0to42pr  13648  fzo1to4tp  13649  fldiv4p1lem1div2  13734  sq4e2t8  14101  i4  14106  crreczi  14130  fac1  14179  fac3  14182  hashkf  14234  hashinf  14237  dmhashres  14243  hashun3  14286  dmtrclfv  14920  abs0  15187  absi  15188  trirecip  15765  geoihalfsum  15784  esum  15982  tan0  16055  coshval  16059  ef01bndlem  16088  3dvds  16237  3dvdsdec  16238  3dvds2dec  16239  sadc0  16360  3lcm2e6woprm  16521  6lcm4e12  16522  lcmf0  16540  prmo0  16943  gcdmodi  16981  karatsuba  16990  43prm  17028  139prm  17030  631prm  17033  1259lem1  17037  1259lem2  17038  1259lem3  17039  1259lem4  17040  1259lem5  17041  2503lem1  17043  2503lem2  17044  2503lem3  17045  4001lem1  17047  4001lem2  17048  4001lem3  17049  4001lem4  17050  setsfun  17077  setsfun0  17078  ndxarg  17102  chnccat  18527  ex-chn2  18539  pmtrsn  19426  psgnprfval1  19429  sylow2a  19526  ablfac1eu  19982  sralem  21105  pzriprng1ALT  21428  opsrtoslem2  21986  ply1plusgfvi  22149  pf1rcl  22259  restcld  23082  neitr  23090  txbasval  23516  txindis  23544  cnmpt1st  23578  cnmpt2nd  23579  ufildr  23841  restmetu  24480  cphipval2  25163  reust  25303  ehl0base  25338  ismbl  25449  mbfimaopnlem  25578  itg10  25611  itg2cnlem2  25685  itgz  25704  dvmptid  25883  cos2pi  26407  tan4thpi  26445  tan4thpiOLD  26446  sincos6thpi  26447  pige3ALT  26451  dfrelog  26496  logm1  26520  dvlog  26582  efopnlem2  26588  cxpexp  26599  root1id  26686  sqrt2cxp2logb9e3  26731  ang180lem2  26742  1cubrlem  26773  quart1  26788  atandm2  26809  efiasin  26820  asinsinlem  26823  asinsin  26824  asin1  26826  acos1  26827  atancj  26842  atanlogsublem  26847  efiatan2  26849  2efiatan  26850  tanatan  26851  dvatan  26867  log2cnv  26876  log2ublem2  26879  log2ublem3  26880  birthday  26886  basellem8  27020  cht1  27097  chp1  27099  ppi1i  27100  ppi2i  27101  cht2  27104  cht3  27105  bclbnd  27213  bposlem8  27224  2lgslem3c  27331  2lgslem3d  27332  noetasuplem2  27668  noetasuplem3  27669  noetasuplem4  27670  noetainflem4  27674  bday0s  27767  old0  27795  new0  27814  left1s  27835  right1s  27836  sltlpss  27848  slelss  27849  mulsproplem13  28062  mulsproplem14  28063  precsexlem1  28140  precsexlem2  28141  onsiso  28200  bdayn0sf1o  28290  ax5seglem7  28908  axlowdimlem8  28922  axlowdimlem11  28925  vtxvalsnop  29014  iedgvalsnop  29015  umgrislfupgrlem  29095  usgrexmpledg  29235  usgredgffibi  29297  vdegp1bi  29511  edginwlk  29608  uhgrwkspthlem2  29727  clwwlkvbij  30085  wlk2v2elem2  30128  frgrwopreglem3  30286  ex-dif  30395  ex-xp  30408  ex-rn  30412  ex-lcm  30430  ex-prmo  30431  ip0i  30797  ip1ilem  30798  ipdirilem  30801  ipasslem10  30811  hvnegdii  31034  hvaddcani  31037  hvsubaddi  31038  hisubcomi  31076  normlem0  31081  normlem3  31084  normlem9  31090  bcseqi  31092  norm0  31100  norm-ii-i  31109  norm3difi  31119  normpari  31126  normpar2i  31128  polid2i  31129  shs0i  31421  chj0i  31427  pjsslem  31651  ho0subi  31767  hoaddsubi  31793  hosd1i  31794  hopncani  31796  nmop0  31958  nmfn0  31959  lnopunilem1  31982  lnophmlem2  31989  opsqrlem2  32113  pjclem1  32167  atabsi  32373  dmdbr6ati  32395  inin  32488  iuninc  32532  gtiso  32674  f1od2  32694  fpwrelmapffs  32709  fzodif1  32767  nn0split01  32792  dfdec100  32805  dp20u  32850  dp3mul10  32870  dpmul1000  32871  dpexpp1  32880  dpadd2  32882  dpmul  32885  dpmul4  32886  1mhdrd  32888  cycpmrn  33104  tocyccntz  33105  cos9thpiminplylem4  33790  cos9thpiminplylem5  33791  lmat22det  33827  ordtcnvNEW  33925  ordtrest2NEW  33928  zlmtset  33968  qqhucn  33997  esumnul  34053  mbfmcst  34264  carsggect  34323  eulerpartgbij  34377  eulerpartlemn  34386  fib0  34404  fib1  34405  fib2  34407  fib3  34408  fib4  34409  fib5  34410  fib6  34411  0rrv  34456  coinflipprob  34485  ballotlem2  34494  ballotth  34543  signsvf0  34585  itgexpif  34611  hgt750lem  34656  hgt750lem2  34657  bnj1416  35043  r11  35097  r12  35098  derang0  35205  subfac0  35213  subfac1  35214  satfv1  35399  fmla  35417  fmla0  35418  fmla0xp  35419  fmla1  35423  mthmpps  35618  problem2  35702  quad3  35706  dfrdg2  35829  pprodcnveq  35917  dffv5  35958  fullfunfv  35981  ellines  36186  rankeq1o  36205  onint1  36483  bj-xpimasn  36989  bj-pr11val  37039  bj-pr21val  37047  bj-pr22val  37053  bj-nuliotaALT  37092  bj-dfmpoa  37152  bj-opabco  37222  icorempo  37385  finxpreclem4  37428  finxp2o  37433  finxp3o  37434  matunitlindf  37658  poimirlem5  37665  poimirlem22  37682  poimirlem26  37686  poimirlem30  37690  ismblfin  37701  dvtan  37710  asindmre  37743  dvasin  37744  dvacos  37745  areacirclem5  37752  heiborlem6  37856  dmcnvep  38407  dmxrncnvep  38408  xrnres4  38437  dfcoels  38467  coss0  38516  refsymrels2  38602  dfeqvrels2  38625  refrelsredund4  38669  hdmap1cbv  41841  lcm4un  42049  lcm5un  42050  lcm6un  42051  lcm7un  42052  lcm8un  42053  3lexlogpow5ineq1  42087  5bc2eq10  42175  imaopab  42264  decpmul  42321  cxpi11d  42376  tan3rdpi  42385  sin2t3rdpi  42386  cos2t3rdpi  42387  readvrec2  42394  remul02  42438  fltnltalem  42695  sum9cubes  42705  diophrw  42792  dnwech  43081  lmhmlnmsplit  43120  fgraphopab  43236  arearect  43248  areaquad  43249  oaomoencom  43350  dmnonrel  43623  imanonrel  43626  cononrel1  43627  cononrel2  43628  rclexi  43648  rtrclex  43650  dfrtrcl5  43662  sqrtcval  43674  resqrtvalex  43678  imsqrtvalex  43679  cnvtrrel  43703  dfrcl2  43707  dfrcl4  43709  iunrelexp0  43735  comptiunov2i  43739  relexpaddss  43751  brtrclfv2  43760  trclfvdecomr  43761  corcltrcl  43772  cotrclrcl  43775  fsovcnvlem  44046  neicvgnvo  44148  scottabf  44273  mnuprdlem1  44305  hashnzfz  44353  lhe4.4ex1a  44362  tgqioo2  45587  sumnnodd  45670  limsup0  45732  limsup10ex  45811  liminf10ex  45812  cosnegpi  45905  itgsin0pilem1  45988  stoweidlem13  46051  wallispilem4  46106  wallispi2lem1  46109  wallispi2lem2  46110  stirlinglem3  46114  dirkertrigeqlem1  46136  fourierdlem56  46200  fourierdlem57  46201  fourierdlem58  46202  fourierdlem62  46206  fourierdlem103  46247  fourierdlem104  46248  fourierdlem112  46256  sqwvfoura  46266  fouriersw  46269  etransclem23  46295  etransclem36  46308  etransclem38  46310  carageniuncllem1  46559  0ome  46567  ovn02  46606  smflimlem4  46812  smflim  46815  smflim2  46844  smflimsup  46866  smfliminf  46869  fmtno0  47571  fmtno1  47572  fmtno2  47581  fmtno3  47582  fmtno4  47583  fmtno5lem4  47587  139prmALT  47627  31prm  47628  5tcu2e40  47646  3exp4mod41  47647  41prothprmlem2  47649  41prothprm  47650  nnsum3primesgbe  47823  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  nnsum4primeseven  47831  nnsum4primesevenALTV  47832  bgoldbtbndlem1  47836  tgoldbachlt  47847  isuspgrim0lem  47924  isubgr3stgrlem4  48000  isubgr3stgrlem6  48002  isubgr3stgrlem7  48003  usgrexmpl1vtx  48054  usgrexmpl1edg  48055  usgrexmpl2vtx  48059  usgrexmpl2edg  48060  gpg5gricstgr3  48121  gpgprismgr4cycllem7  48132  cznrnglem  48290  2t6m3t4e0  48379  zlmodzxzldeplem3  48534  ackval0  48712  ackval1  48713  ackval2  48714  ackval3  48715  ackval40  48725  ackval42  48728  ackval50  48730  disjdifb  48841  dftpos6  48906  tposresg  48909  tposrescnv  48910  tposres3  48912  tposid  48916  iscnrm3rlem1  48971  dfswapf2  49293  setc1onsubc  49634  sec0  49792