Theorem 3eqtri 2790

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  csbid  3866  csbconstg  3872  csbie  3888  un23  4127  in32  4182  dfnul4  4288  unvdif  4436  undif2  4438  undifabs  4439  difun2  4442  difdifdir  4452  dfif4  4503  dfif5  4504  tpidm23  4723  dfopif  4835  dfiunv2  4998  symdif0  5051  symdifv  5052  symdifid  5053  unidif0  5330  unidif0OLD  5331  uniop  5498  xpun  5735  dfrn2  5878  dfdmf  5886  dfrnf  5940  res0  5982  resres  5991  xpssres  6017  dfima2  6064  imai  6076  ima0  6079  imaundir  6148  xpima  6180  cnvrescnv  6194  dmresv  6199  rescnvcnv  6205  dmtpop  6219  rnsnopg  6222  resdmres  6233  resdifdi  6237  dmmpt  6241  dmco  6256  co01  6263  suc0  6438  iunsuc  6448  fresaun  6749  dffv4  6878  f1ossf1o  7124  fpr  7151  mpo0  7495  dmoprab  7513  rnoprab  7515  elrnmpores  7548  ov6g  7574  1st0  7988  2nd0  7989  dfmpo  8093  curry1  8095  curry2  8098  fpar  8107  dftpos2  8235  tposoprab  8254  tposmpo  8255  fvmpocurryd  8263  frrlem14  8292  dfrecs3  8355  tfrlem8  8367  seqomlem3  8435  df2o3  8457  nlim2  8471  omxpenlem  9062  dfsdom2  9084  pwfir  9272  marypha2lem2  9392  sup00  9421  epinid0  9563  scottexs  9857  scott0s  9858  scottabf  9862  infxpenc2  10002  kmlem3  10132  ackbij1lem2  10199  compsscnv  10350  fin1a2lem12  10390  mulerpqlem  10935  1lt2nq  10953  axi2m1  11139  2p2e4  12370  numsuc  12720  numsucc  12751  decmul10add  12780  5p5e10  12782  6p4e10  12783  7p3e10  12786  xnegmnf  13231  pnfaddmnf  13251  fz12pr  13605  fz0tp  13652  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzo13pr  13774  fzo0to2pr  13775  fz01pr  13776  fzo0to3tp  13777  fzo0to42pr  13778  fzo1to4tp  13779  fldiv4p1lem1div2  13864  sq4e2t8  14231  i4  14236  crreczi  14260  fac1  14309  fac3  14312  hashkf  14364  hashinf  14367  dmhashres  14373  hashun3  14416  dmtrclfv  15051  abs0  15332  absi  15333  trirecip  15913  geoihalfsum  15932  esum  16129  tan0  16202  coshval  16206  ef01bndlem  16235  3dvds  16384  3dvdsdec  16385  3dvds2dec  16386  sadc0  16507  3lcm2e6woprm  16668  6lcm4e12  16669  lcmf0  16687  prmo0  17091  prmo3  17096  gcdmodi  17129  karatsuba  17138  43prm  17177  139prm  17179  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  2503lem3  17194  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  setsfun  17226  setsfun0  17227  ndxarg  17251  chnccat  18677  ex-chn2  18689  pmtrsn  19584  psgnprfval1  19587  sylow2a  19684  ablfac1eu  20140  sralem  21297  pzriprng1ALT  21646  opsrtoslem2  22207  ply1plusgfvi  22401  pf1rcl  22509  restcld  23329  neitr  23337  txbasval  23763  txindis  23791  cnmpt1st  23825  cnmpt2nd  23826  ufildr  24088  restmetu  24727  cphipval2  25400  reust  25540  ehl0base  25575  ismbl  25685  mbfimaopnlem  25814  itg10  25847  itg2cnlem2  25921  itgz  25940  dvmptid  26116  cos2pi  26641  tan4thpi  26679  tan4thpiOLD  26680  sincos6thpi  26681  pige3ALT  26685  dfrelog  26730  logm1  26754  dvlog  26816  efopnlem2  26822  cxpexp  26833  root1id  26919  sqrt2cxp2logb9e3  26964  ang180lem2  26975  1cubrlem  27006  quart1  27021  atandm2  27042  efiasin  27053  asinsinlem  27056  asinsin  27057  asin1  27059  acos1  27060  atancj  27075  atanlogsublem  27080  efiatan2  27082  2efiatan  27083  tanatan  27084  dvatan  27100  log2cnv  27109  log2ublem2  27112  log2ublem3  27113  birthday  27119  basellem8  27252  cht1  27329  chp1  27331  ppi1i  27332  ppi2i  27333  cht2  27336  cht3  27337  bclbnd  27444  bposlem8  27455  2lgslem3c  27562  2lgslem3d  27563  noetasuplem2  27898  noetasuplem3  27899  noetasuplem4  27900  noetainflem4  27904  bday0  28004  old0  28032  new0  28057  left1s  28088  right1s  28089  ltslpss  28101  leslss  28102  mulsproplem13  28321  mulsproplem14  28322  precsexlem1  28400  precsexlem2  28401  oniso  28464  bdayn0sf1o  28563  ax5seglem7  29285  axlowdimlem8  29299  axlowdimlem11  29302  vtxvalsnop  29391  iedgvalsnop  29392  umgrislfupgrlem  29472  usgrexmpledg  29612  usgredgffibi  29674  vdegp1bi  29887  edginwlk  29984  uhgrwkspthlem2  30103  clwwlkvbij  30464  wlk2v2elem2  30507  frgrwopreglem3  30665  ex-dif  30774  ex-xp  30787  ex-rn  30791  ex-lcm  30809  ex-prmo  30810  ip0i  31177  ip1ilem  31178  ipdirilem  31181  ipasslem10  31191  hvnegdii  31414  hvaddcani  31417  hvsubaddi  31418  hisubcomi  31456  normlem0  31461  normlem3  31464  normlem9  31470  bcseqi  31472  norm0  31480  norm-ii-i  31489  norm3difi  31499  normpari  31506  normpar2i  31508  polid2i  31509  shs0i  31801  chj0i  31807  pjsslem  32031  ho0subi  32147  hoaddsubi  32173  hosd1i  32174  hopncani  32176  nmop0  32338  nmfn0  32339  lnopunilem1  32362  lnophmlem2  32369  opsqrlem2  32493  pjclem1  32547  atabsi  32753  dmdbr6ati  32775  inin  32862  iuninc  32905  gtiso  33046  f1od2  33064  fpwrelmapffs  33079  fzodif1  33137  nn0split01  33162  dfdec100  33174  dp20u  33197  dp3mul10  33217  dpmul1000  33218  dpexpp1  33227  dpadd2  33229  dpmul  33232  dpmul4  33233  1mhdrd  33235  cycpmrn  33463  tocyccntz  33464  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  lmat22det  34212  ordtcnvNEW  34310  ordtrest2NEW  34313  zlmtset  34353  qqhucn  34382  esumnul  34438  mbfmcst  34649  carsggect  34708  eulerpartgbij  34762  eulerpartlemn  34771  fib0  34789  fib1  34790  fib2  34792  fib3  34793  fib4  34794  fib5  34795  fib6  34796  0rrv  34841  coinflipprob  34870  ballotlem2  34879  ballotth  34928  signsvf0  34967  itgexpif  34993  hgt750lem  35038  hgt750lem2  35039  bnj1416  35427  r11  35487  r12  35488  derang0  35661  subfac0  35669  subfac1  35670  satfv1  35855  fmla  35873  fmla0  35874  fmla0xp  35875  fmla1  35879  mthmpps  36074  problem2  36158  quad3  36162  dfrdg2  36285  pprodcnveq  36373  dffv5  36414  dfsuccf2  36433  fullfunfv  36439  ellines  36644  rankeq1o  36663  onint1  36960  bj-xpimasn  37591  bj-pr11val  37641  bj-pr21val  37649  bj-pr22val  37655  bj-nuliotaALT  37694  bj-dfmpoa  37760  bj-opabco  37832  icorempo  37997  finxpreclem4  38040  finxp2o  38045  finxp3o  38046  matunitlindf  38269  poimirlem5  38276  poimirlem22  38293  poimirlem26  38297  poimirlem30  38301  ismblfin  38312  dvtan  38321  asindmre  38354  dvasin  38355  dvacos  38356  areacirclem5  38363  heiborlem6  38467  dmcnvep  39037  dmxrncnvep  39038  dmcnvepres  39039  dmxrnuncnvepres  39041  xrnres4  39077  dfadjliftmap2  39106  blockadjliftmap  39107  dfblockliftmap2  39110  dfsucmap3  39112  dfsuccl2  39119  dfcoels  39169  coss0  39218  refsymrels2  39298  dfeqvrels2  39321  refrelsredund4  39365  hdmap1cbv  42576  lcm4un  42783  lcm5un  42784  lcm6un  42785  lcm7un  42786  lcm8un  42787  3lexlogpow5ineq1  42821  5bc2eq10  42909  imaopab  43002  decpmul  43049  cxpi11d  43104  tan3rdpi  43113  sin2t3rdpi  43114  cos2t3rdpi  43115  readvrec2  43122  remul02  43166  fltnltalem  43394  sum9cubes  43404  diophrw  43490  dnwech  43775  lmhmlnmsplit  43814  fgraphopab  43930  arearect  43942  areaquad  43943  oaomoencom  44044  dmnonrel  44316  imanonrel  44319  cononrel1  44320  cononrel2  44321  rclexi  44341  rtrclex  44343  dfrtrcl5  44355  sqrtcval  44367  resqrtvalex  44371  imsqrtvalex  44372  cnvtrrel  44396  dfrcl2  44400  dfrcl4  44402  iunrelexp0  44428  comptiunov2i  44432  relexpaddss  44444  brtrclfv2  44453  trclfvdecomr  44454  corcltrcl  44465  cotrclrcl  44468  fsovcnvlem  44739  neicvgnvo  44841  mnuprdlem1  44982  hashnzfz  45030  lhe4.4ex1a  45039  tgqioo2  46263  sumnnodd  46346  limsup0  46408  limsup10ex  46487  liminf10ex  46488  cosnegpi  46581  itgsin0pilem1  46664  stoweidlem13  46727  wallispilem4  46782  wallispi2lem1  46785  wallispi2lem2  46786  stirlinglem3  46790  dirkertrigeqlem1  46812  fourierdlem56  46876  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fourierdlem103  46923  fourierdlem104  46924  fourierdlem112  46932  sqwvfoura  46942  fouriersw  46945  etransclem23  46971  etransclem36  46984  etransclem38  46986  carageniuncllem1  47235  0ome  47243  ovn02  47282  smflimlem4  47488  smflim  47491  smflim2  47520  smflimsup  47542  smfliminf  47545  nthrucw  47607  cos5t  47616  goldratmolem2  47623  fmtno0  48292  fmtno1  48293  fmtno2  48302  fmtno3  48303  fmtno4  48304  fmtno5lem4  48308  139prmALT  48348  31prm  48349  5tcu2e40  48367  3exp4mod41  48368  41prothprmlem2  48370  41prothprm  48371  ppivalnn4  48379  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  bgoldbtbndlem1  48570  tgoldbachlt  48581  isuspgrim0lem  48658  isubgr3stgrlem4  48734  isubgr3stgrlem6  48736  isubgr3stgrlem7  48737  usgrexmpl1vtx  48788  usgrexmpl1edg  48789  usgrexmpl2vtx  48793  usgrexmpl2edg  48794  gpg5gricstgr3  48855  gpgprismgr4cycllem7  48866  cznrnglem  49024  2t6m3t4e0  49128  zlmodzxzldeplem3  49282  ackval0  49460  ackval1  49461  ackval2  49462  ackval3  49463  ackval40  49473  ackval42  49476  ackval50  49478  disjdifb  49588  dftpos6  49653  tposresg  49656  tposrescnv  49657  tposres3  49659  tposid  49663  iscnrm3rlem1  49718  dfswapf2  50039  setc1onsubc  50380  sec0  50538