Theorem 3eqtri 2825

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  csbid  3841  un23  4095  in32  4148  dfnul2  4245  unvdif  4381  undif2  4383  undifabs  4384  difun2  4387  difdifdir  4395  dfif4  4440  dfif5  4441  tpidm23  4653  dfopif  4760  dfiunv2  4922  symdif0  4970  symdifid  4972  unidif0  5225  uniop  5370  xpun  5589  dfrn2  5723  dfdmf  5729  dfrnf  5784  res0  5822  resres  5831  xpssres  5855  dfima2  5898  imai  5909  ima0  5912  imaundir  5976  xpima  6006  cnvrescnv  6019  dmresv  6024  rescnvcnv  6028  dmtpop  6042  rnsnopg  6045  resdmres  6056  dmmpt  6061  dmco  6074  co01  6081  suc0  6233  unisuc  6235  iunsuc  6241  fresaun  6523  dffv4  6642  fvssunirn  6674  f1ossf1o  6867  fpr  6893  mpo0  7218  dmoprab  7234  rnoprab  7236  elrnmpores  7267  ov6g  7292  1st0  7677  2nd0  7678  dfmpo  7780  curry1  7782  curry2  7785  fpar  7794  algrflem  7802  dftpos2  7892  tposoprab  7911  tposmpo  7912  fvmpocurryd  7920  wfrlem14  7951  wfrlem16  7953  dfrecs3  7992  tfrlem8  8003  seqomlem3  8071  df2o3  8100  omxpenlem  8601  dfsdom2  8624  marypha2lem2  8884  sup00  8912  epinid0  9048  scottexs  9300  scott0s  9301  infxpenc2  9433  kmlem3  9563  ackbij1lem2  9632  compsscnv  9782  fin1a2lem12  9822  mulerpqlem  10366  1lt2nq  10384  axi2m1  10570  2p2e4  11760  numsuc  12100  numsucc  12126  decmul10add  12155  5p5e10  12157  6p4e10  12158  7p3e10  12161  xnegmnf  12591  pnfaddmnf  12611  fz12pr  12959  fz0tp  13003  fz0to3un2pr  13004  fzo13pr  13116  fzo0to2pr  13117  fzo0to3tp  13118  fzo0to42pr  13119  fzo1to4tp  13120  fldiv4p1lem1div2  13200  sq4e2t8  13558  i4  13563  crreczi  13585  fac1  13633  fac3  13636  hashkf  13688  hashinf  13691  dmhashres  13697  hashun3  13741  cshwsexa  14177  dmtrclfv  14369  abs0  14637  absi  14638  trirecip  15210  geoihalfsum  15230  esum  15426  tan0  15496  coshval  15500  ef01bndlem  15529  3dvds  15672  3dvdsdec  15673  3dvds2dec  15674  sadc0  15793  3lcm2e6woprm  15949  6lcm4e12  15950  lcmf0  15968  prmo0  16362  gcdmodi  16400  karatsuba  16410  43prm  16447  139prm  16449  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  ndxarg  16500  setsfun  16510  setsfun0  16511  pmtrsn  18639  psgnprfval1  18642  sylow2a  18736  ablfac1eu  19188  sralem  19942  opsrtoslem2  20724  ply1plusgfvi  20871  pf1rcl  20973  restcld  21777  neitr  21785  txbasval  22211  txindis  22239  cnmpt1st  22273  cnmpt2nd  22274  ufildr  22536  restmetu  23177  cphipval2  23845  reust  23985  ehl0base  24020  ismbl  24130  mbfimaopnlem  24259  itg10  24292  itg2cnlem2  24366  itgz  24384  dvmptid  24560  cos2pi  25069  tan4thpi  25107  sincos6thpi  25108  pige3ALT  25112  dfrelog  25157  logm1  25180  dvlog  25242  efopnlem2  25248  cxpexp  25259  root1id  25343  sqrt2cxp2logb9e3  25385  ang180lem2  25396  1cubrlem  25427  quart1  25442  atandm2  25463  efiasin  25474  asinsinlem  25477  asinsin  25478  asin1  25480  acos1  25481  atancj  25496  atanlogsublem  25501  efiatan2  25503  2efiatan  25504  tanatan  25505  dvatan  25521  log2cnv  25530  log2ublem2  25533  log2ublem3  25534  birthday  25540  basellem8  25673  cht1  25750  chp1  25752  ppi1i  25753  ppi2i  25754  cht2  25757  cht3  25758  bclbnd  25864  bposlem8  25875  2lgslem3c  25982  2lgslem3d  25983  ax5seglem7  26729  axlowdimlem8  26743  axlowdimlem11  26746  vtxvalsnop  26834  iedgvalsnop  26835  umgrislfupgrlem  26915  usgrexmpledg  27052  usgredgffibi  27114  vdegp1bi  27327  edginwlk  27424  uhgrwkspthlem2  27543  clwwlkvbij  27898  wlk2v2elem2  27941  frgrwopreglem3  28099  ex-dif  28208  ex-xp  28221  ex-rn  28225  ex-lcm  28243  ex-prmo  28244  ip0i  28608  ip1ilem  28609  ipdirilem  28612  ipasslem10  28622  hvnegdii  28845  hvaddcani  28848  hvsubaddi  28849  hisubcomi  28887  normlem0  28892  normlem3  28895  normlem9  28901  bcseqi  28903  norm0  28911  norm-ii-i  28920  norm3difi  28930  normpari  28937  normpar2i  28939  polid2i  28940  shs0i  29232  chj0i  29238  pjsslem  29462  ho0subi  29578  hoaddsubi  29604  hosd1i  29605  hopncani  29607  nmop0  29769  nmfn0  29770  lnopunilem1  29793  lnophmlem2  29800  opsqrlem2  29924  pjclem1  29978  atabsi  30184  dmdbr6ati  30206  inin  30286  iuninc  30324  gtiso  30460  f1od2  30483  fpwrelmapffs  30496  fzodif1  30542  dfdec100  30572  dp20u  30580  dp3mul10  30600  dpmul1000  30601  dpexpp1  30610  dpadd2  30612  dpmul  30615  dpmul4  30616  1mhdrd  30618  cycpmrn  30835  tocyccntz  30836  lmat22det  31175  ordtcnvNEW  31273  ordtrest2NEW  31276  zlmtset  31316  qqhucn  31343  esumnul  31417  mbfmcst  31627  carsggect  31686  eulerpartgbij  31740  eulerpartlemn  31749  fib0  31767  fib1  31768  fib2  31770  fib3  31771  fib4  31772  fib5  31773  fib6  31774  0rrv  31819  coinflipprob  31847  ballotlem2  31856  ballotth  31905  signsvf0  31960  itgexpif  31987  hgt750lem  32032  hgt750lem2  32033  bnj1416  32421  derang0  32529  subfac0  32537  subfac1  32538  satfv1  32723  fmla  32741  fmla0  32742  fmla0xp  32743  fmla1  32747  mthmpps  32942  problem2  33022  quad3  33026  dfrdg2  33153  trpred0  33188  frrlem14  33249  noetalem2  33331  noetalem3  33332  pprodcnveq  33457  dffv5  33498  fullfunfv  33521  ellines  33726  rankeq1o  33745  onint1  33910  bj-xpimasn  34391  bj-pr11val  34441  bj-pr21val  34449  bj-pr22val  34455  bj-nuliotaALT  34475  bj-dfmpoa  34533  bj-opabco  34603  icorempo  34768  finxpreclem4  34811  finxp2o  34816  finxp3o  34817  matunitlindf  35055  poimirlem5  35062  poimirlem22  35079  poimirlem26  35083  poimirlem30  35087  ismblfin  35098  dvtan  35107  asindmre  35140  dvasin  35141  dvacos  35142  areacirclem5  35149  heiborlem6  35254  xrnres4  35813  dfcoels  35835  coss0  35879  refsymrels2  35961  dfeqvrels2  35983  refrelsredund4  36027  hdmap1cbv  39098  lcm4un  39304  lcm5un  39305  lcm6un  39306  lcm7un  39307  lcm8un  39308  5bc2eq10  39346  2xp3dxp2ge1d  39387  imaopab  39413  sqn5ii  39480  decpmul  39482  remul02  39543  rei4  39560  sn-0lt1  39587  fltnltalem  39618  diophrw  39700  dnwech  39992  lmhmlnmsplit  40031  fgraphopab  40154  arearect  40165  areaquad  40166  dmnonrel  40290  imanonrel  40293  cononrel1  40294  cononrel2  40295  rclexi  40315  rtrclex  40317  dfrtrcl5  40329  sqrtcval  40341  resqrtvalex  40345  imsqrtvalex  40346  cnvtrrel  40371  dfrcl2  40375  dfrcl4  40377  iunrelexp0  40403  comptiunov2i  40407  relexpaddss  40419  brtrclfv2  40428  trclfvdecomr  40429  corcltrcl  40440  cotrclrcl  40443  fsovcnvlem  40714  neicvgnvo  40818  scottabf  40948  mnuprdlem1  40980  hashnzfz  41024  lhe4.4ex1a  41033  tgqioo2  42184  sumnnodd  42272  limsup0  42336  limsup10ex  42415  liminf10ex  42416  cosnegpi  42509  itgsin0pilem1  42592  stoweidlem13  42655  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem3  42718  dirkertrigeqlem1  42740  fourierdlem56  42804  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  sqwvfoura  42870  fouriersw  42873  etransclem23  42899  etransclem36  42912  etransclem38  42914  carageniuncllem1  43160  0ome  43168  ovn02  43207  smflimlem4  43407  smflim  43410  smflim2  43437  smflimsup  43459  smfliminf  43462  fmtno0  44057  fmtno1  44058  fmtno2  44067  fmtno3  44068  fmtno4  44069  fmtno5lem4  44073  139prmALT  44113  31prm  44114  5tcu2e40  44133  3exp4mod41  44134  41prothprmlem2  44136  41prothprm  44137  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  tgoldbachlt  44334  cznrnglem  44577  2t6m3t4e0  44750  zlmodzxzldeplem3  44911  ackval0  45094  ackval1  45095  ackval2  45096  ackval3  45097  ackval40  45107  ackval42  45110  ackval50  45112  sec0  45286