Theorem 3eqtri 2763

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  csbid  3850  csbconstg  3856  csbie  3872  un23  4114  in32  4170  dfnul4  4275  unvdif  4415  undif2  4417  undifabs  4418  difun2  4421  difdifdir  4431  dfif4  4482  dfif5  4483  tpidm23  4701  dfopif  4813  dfiunv2  4976  symdif0  5027  symdifv  5028  symdifid  5029  unidif0  5301  unidif0OLD  5302  uniop  5469  xpun  5705  dfrn2  5843  dfdmf  5851  dfrnf  5905  res0  5948  resres  5957  xpssres  5983  dfima2  6027  imai  6039  ima0  6042  imaundir  6114  xpima  6146  cnvrescnv  6159  dmresv  6164  rescnvcnv  6168  dmtpop  6182  rnsnopg  6185  resdmres  6196  resdifdi  6200  dmmpt  6204  dmco  6219  co01  6226  suc0  6400  iunsuc  6410  fresaun  6711  dffv4  6837  f1ossf1o  7081  fpr  7108  mpo0  7452  dmoprab  7470  rnoprab  7472  elrnmpores  7505  ov6g  7531  1st0  7948  2nd0  7949  dfmpo  8052  curry1  8054  curry2  8057  fpar  8066  dftpos2  8193  tposoprab  8212  tposmpo  8213  fvmpocurryd  8221  frrlem14  8249  dfrecs3  8312  tfrlem8  8323  seqomlem3  8391  df2o3  8413  nlim2  8425  omxpenlem  9016  dfsdom2  9038  pwfir  9227  marypha2lem2  9349  sup00  9378  epinid0  9519  scottexs  9811  scott0s  9812  infxpenc2  9944  kmlem3  10075  ackbij1lem2  10142  compsscnv  10293  fin1a2lem12  10333  mulerpqlem  10878  1lt2nq  10896  axi2m1  11082  2p2e4  12311  numsuc  12658  numsucc  12684  decmul10add  12713  5p5e10  12715  6p4e10  12716  7p3e10  12719  xnegmnf  13162  pnfaddmnf  13182  fz12pr  13535  fz0tp  13582  fz0to3un2pr  13583  fz0to4untppr  13584  fz0to5un2tp  13585  fzo13pr  13704  fzo0to2pr  13705  fz01pr  13706  fzo0to3tp  13707  fzo0to42pr  13708  fzo1to4tp  13709  fldiv4p1lem1div2  13794  sq4e2t8  14161  i4  14166  crreczi  14190  fac1  14239  fac3  14242  hashkf  14294  hashinf  14297  dmhashres  14303  hashun3  14346  dmtrclfv  14980  abs0  15247  absi  15248  trirecip  15828  geoihalfsum  15847  esum  16045  tan0  16118  coshval  16122  ef01bndlem  16151  3dvds  16300  3dvdsdec  16301  3dvds2dec  16302  sadc0  16423  3lcm2e6woprm  16584  6lcm4e12  16585  lcmf0  16603  prmo0  17007  gcdmodi  17045  karatsuba  17054  43prm  17092  139prm  17094  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  setsfun  17141  setsfun0  17142  ndxarg  17166  chnccat  18592  ex-chn2  18604  pmtrsn  19494  psgnprfval1  19497  sylow2a  19594  ablfac1eu  20050  sralem  21171  pzriprng1ALT  21476  opsrtoslem2  22034  ply1plusgfvi  22205  pf1rcl  22314  restcld  23137  neitr  23145  txbasval  23571  txindis  23599  cnmpt1st  23633  cnmpt2nd  23634  ufildr  23896  restmetu  24535  cphipval2  25208  reust  25348  ehl0base  25383  ismbl  25493  mbfimaopnlem  25622  itg10  25655  itg2cnlem2  25729  itgz  25748  dvmptid  25924  cos2pi  26440  tan4thpi  26478  tan4thpiOLD  26479  sincos6thpi  26480  pige3ALT  26484  dfrelog  26529  logm1  26553  dvlog  26615  efopnlem2  26621  cxpexp  26632  root1id  26718  sqrt2cxp2logb9e3  26763  ang180lem2  26774  1cubrlem  26805  quart1  26820  atandm2  26841  efiasin  26852  asinsinlem  26855  asinsin  26856  asin1  26858  acos1  26859  atancj  26874  atanlogsublem  26879  efiatan2  26881  2efiatan  26882  tanatan  26883  dvatan  26899  log2cnv  26908  log2ublem2  26911  log2ublem3  26912  birthday  26918  basellem8  27051  cht1  27128  chp1  27130  ppi1i  27131  ppi2i  27132  cht2  27135  cht3  27136  bclbnd  27243  bposlem8  27254  2lgslem3c  27361  2lgslem3d  27362  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem4  27704  bday0  27803  old0  27831  new0  27856  left1s  27887  right1s  27888  ltslpss  27900  leslss  27901  mulsproplem13  28120  mulsproplem14  28121  precsexlem1  28199  precsexlem2  28200  oniso  28263  bdayn0sf1o  28362  ax5seglem7  29004  axlowdimlem8  29018  axlowdimlem11  29021  vtxvalsnop  29110  iedgvalsnop  29111  umgrislfupgrlem  29191  usgrexmpledg  29331  usgredgffibi  29393  vdegp1bi  29606  edginwlk  29703  uhgrwkspthlem2  29822  clwwlkvbij  30183  wlk2v2elem2  30226  frgrwopreglem3  30384  ex-dif  30493  ex-xp  30506  ex-rn  30510  ex-lcm  30528  ex-prmo  30529  ip0i  30896  ip1ilem  30897  ipdirilem  30900  ipasslem10  30910  hvnegdii  31133  hvaddcani  31136  hvsubaddi  31137  hisubcomi  31175  normlem0  31180  normlem3  31183  normlem9  31189  bcseqi  31191  norm0  31199  norm-ii-i  31208  norm3difi  31218  normpari  31225  normpar2i  31227  polid2i  31228  shs0i  31520  chj0i  31526  pjsslem  31750  ho0subi  31866  hoaddsubi  31892  hosd1i  31893  hopncani  31895  nmop0  32057  nmfn0  32058  lnopunilem1  32081  lnophmlem2  32088  opsqrlem2  32212  pjclem1  32266  atabsi  32472  dmdbr6ati  32494  inin  32586  iuninc  32630  gtiso  32774  f1od2  32792  fpwrelmapffs  32807  fzodif1  32865  nn0split01  32891  dfdec100  32903  dp20u  32937  dp3mul10  32957  dpmul1000  32958  dpexpp1  32967  dpadd2  32969  dpmul  32972  dpmul4  32973  1mhdrd  32975  cycpmrn  33204  tocyccntz  33205  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  lmat22det  33966  ordtcnvNEW  34064  ordtrest2NEW  34067  zlmtset  34107  qqhucn  34136  esumnul  34192  mbfmcst  34403  carsggect  34462  eulerpartgbij  34516  eulerpartlemn  34525  fib0  34543  fib1  34544  fib2  34546  fib3  34547  fib4  34548  fib5  34549  fib6  34550  0rrv  34595  coinflipprob  34624  ballotlem2  34633  ballotth  34682  signsvf0  34724  itgexpif  34750  hgt750lem  34795  hgt750lem2  34796  bnj1416  35181  r11  35237  r12  35238  derang0  35351  subfac0  35359  subfac1  35360  satfv1  35545  fmla  35563  fmla0  35564  fmla0xp  35565  fmla1  35569  mthmpps  35764  problem2  35848  quad3  35852  dfrdg2  35975  pprodcnveq  36063  dffv5  36104  dfsuccf2  36123  fullfunfv  36129  ellines  36334  rankeq1o  36353  onint1  36631  bj-xpimasn  37262  bj-pr11val  37312  bj-pr21val  37320  bj-pr22val  37326  bj-nuliotaALT  37365  bj-dfmpoa  37430  bj-opabco  37502  icorempo  37667  finxpreclem4  37710  finxp2o  37715  finxp3o  37716  matunitlindf  37939  poimirlem5  37946  poimirlem22  37963  poimirlem26  37967  poimirlem30  37971  ismblfin  37982  dvtan  37991  asindmre  38024  dvasin  38025  dvacos  38026  areacirclem5  38033  heiborlem6  38137  dmcnvep  38709  dmxrncnvep  38710  dmcnvepres  38711  dmxrnuncnvepres  38713  xrnres4  38749  dfadjliftmap2  38778  blockadjliftmap  38779  dfblockliftmap2  38782  dfsucmap3  38784  dfsuccl2  38791  dfcoels  38841  coss0  38890  refsymrels2  38970  dfeqvrels2  38993  refrelsredund4  39037  hdmap1cbv  42248  lcm4un  42455  lcm5un  42456  lcm6un  42457  lcm7un  42458  lcm8un  42459  3lexlogpow5ineq1  42493  5bc2eq10  42581  imaopab  42672  decpmul  42720  cxpi11d  42775  tan3rdpi  42784  sin2t3rdpi  42785  cos2t3rdpi  42786  readvrec2  42793  remul02  42837  fltnltalem  43095  sum9cubes  43105  diophrw  43191  dnwech  43476  lmhmlnmsplit  43515  fgraphopab  43631  arearect  43643  areaquad  43644  oaomoencom  43745  dmnonrel  44017  imanonrel  44020  cononrel1  44021  cononrel2  44022  rclexi  44042  rtrclex  44044  dfrtrcl5  44056  sqrtcval  44068  resqrtvalex  44072  imsqrtvalex  44073  cnvtrrel  44097  dfrcl2  44101  dfrcl4  44103  iunrelexp0  44129  comptiunov2i  44133  relexpaddss  44145  brtrclfv2  44154  trclfvdecomr  44155  corcltrcl  44166  cotrclrcl  44169  fsovcnvlem  44440  neicvgnvo  44542  scottabf  44667  mnuprdlem1  44699  hashnzfz  44747  lhe4.4ex1a  44756  tgqioo2  45977  sumnnodd  46060  limsup0  46122  limsup10ex  46201  liminf10ex  46202  cosnegpi  46295  itgsin0pilem1  46378  stoweidlem13  46441  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem3  46504  dirkertrigeqlem1  46526  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  sqwvfoura  46656  fouriersw  46659  etransclem23  46685  etransclem36  46698  etransclem38  46700  carageniuncllem1  46949  0ome  46957  ovn02  46996  smflimlem4  47202  smflim  47205  smflim2  47234  smflimsup  47256  smfliminf  47259  cos5t  47327  goldratmolem2  47334  fmtno0  48003  fmtno1  48004  fmtno2  48013  fmtno3  48014  fmtno4  48015  fmtno5lem4  48019  139prmALT  48059  31prm  48060  5tcu2e40  48078  3exp4mod41  48079  41prothprmlem2  48081  41prothprm  48082  ppivalnn4  48090  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  tgoldbachlt  48292  isuspgrim0lem  48369  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  usgrexmpl1vtx  48499  usgrexmpl1edg  48500  usgrexmpl2vtx  48504  usgrexmpl2edg  48505  gpg5gricstgr3  48566  gpgprismgr4cycllem7  48577  cznrnglem  48735  2t6m3t4e0  48824  zlmodzxzldeplem3  48978  ackval0  49156  ackval1  49157  ackval2  49158  ackval3  49159  ackval40  49169  ackval42  49172  ackval50  49174  disjdifb  49285  dftpos6  49350  tposresg  49353  tposrescnv  49354  tposres3  49356  tposid  49360  iscnrm3rlem1  49415  dfswapf2  49736  setc1onsubc  50077  sec0  50235