Theorem 3eqtri 2756

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  csbid  3875  csbconstg  3881  csbie  3897  un23  4137  in32  4193  dfnul4  4298  unvdif  4438  undif2  4440  undifabs  4441  difun2  4444  difdifdir  4455  dfif4  4504  dfif5  4505  tpidm23  4721  dfopif  4834  dfiunv2  4999  symdif0  5049  symdifid  5051  unidif0  5315  uniop  5475  xpun  5712  dfrn2  5852  dfdmf  5860  dfrnf  5914  res0  5954  resres  5963  xpssres  5989  dfima2  6033  imai  6045  ima0  6048  imaundir  6123  xpima  6155  cnvrescnv  6168  dmresv  6173  rescnvcnv  6177  dmtpop  6191  rnsnopg  6194  resdmres  6205  resdifdi  6209  dmmpt  6213  dmco  6227  co01  6234  suc0  6409  iunsuc  6419  fresaun  6731  dffv4  6855  fvssunirnOLD  6892  f1ossf1o  7100  fpr  7126  mpo0  7474  dmoprab  7492  rnoprab  7494  elrnmpores  7527  ov6g  7553  1st0  7974  2nd0  7975  dfmpo  8081  curry1  8083  curry2  8086  fpar  8095  dftpos2  8222  tposoprab  8241  tposmpo  8242  fvmpocurryd  8250  frrlem14  8278  dfrecs3  8341  tfrlem8  8352  seqomlem3  8420  df2o3  8442  nlim2  8454  omxpenlem  9042  dfsdom2  9064  pwfir  9266  marypha2lem2  9387  sup00  9416  epinid0  9553  scottexs  9840  scott0s  9841  infxpenc2  9975  kmlem3  10106  ackbij1lem2  10173  compsscnv  10324  fin1a2lem12  10364  mulerpqlem  10908  1lt2nq  10926  axi2m1  11112  2p2e4  12316  numsuc  12663  numsucc  12689  decmul10add  12718  5p5e10  12720  6p4e10  12721  7p3e10  12724  xnegmnf  13170  pnfaddmnf  13190  fz12pr  13542  fz0tp  13589  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  fzo13pr  13710  fzo0to2pr  13711  fz01pr  13712  fzo0to3tp  13713  fzo0to42pr  13714  fzo1to4tp  13715  fldiv4p1lem1div2  13797  sq4e2t8  14164  i4  14169  crreczi  14193  fac1  14242  fac3  14245  hashkf  14297  hashinf  14300  dmhashres  14306  hashun3  14349  cshwsexaOLD  14790  dmtrclfv  14984  abs0  15251  absi  15252  trirecip  15829  geoihalfsum  15848  esum  16046  tan0  16119  coshval  16123  ef01bndlem  16152  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  sadc0  16424  3lcm2e6woprm  16585  6lcm4e12  16586  lcmf0  16604  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  pmtrsn  19449  psgnprfval1  19452  sylow2a  19549  ablfac1eu  20005  sralem  21083  pzriprng1ALT  21406  opsrtoslem2  21963  ply1plusgfvi  22126  pf1rcl  22236  restcld  23059  neitr  23067  txbasval  23493  txindis  23521  cnmpt1st  23555  cnmpt2nd  23556  ufildr  23818  restmetu  24458  cphipval2  25141  reust  25281  ehl0base  25316  ismbl  25427  mbfimaopnlem  25556  itg10  25589  itg2cnlem2  25663  itgz  25682  dvmptid  25861  cos2pi  26385  tan4thpi  26423  tan4thpiOLD  26424  sincos6thpi  26425  pige3ALT  26429  dfrelog  26474  logm1  26498  dvlog  26560  efopnlem2  26566  cxpexp  26577  root1id  26664  sqrt2cxp2logb9e3  26709  ang180lem2  26720  1cubrlem  26751  quart1  26766  atandm2  26787  efiasin  26798  asinsinlem  26801  asinsin  26802  asin1  26804  acos1  26805  atancj  26820  atanlogsublem  26825  efiatan2  26827  2efiatan  26828  tanatan  26829  dvatan  26845  log2cnv  26854  log2ublem2  26857  log2ublem3  26858  birthday  26864  basellem8  26998  cht1  27075  chp1  27077  ppi1i  27078  ppi2i  27079  cht2  27082  cht3  27083  bclbnd  27191  bposlem8  27202  2lgslem3c  27309  2lgslem3d  27310  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem4  27652  bday0s  27740  old0  27767  new0  27786  left1s  27806  right1s  27807  sltlpss  27819  slelss  27820  mulsproplem13  28031  mulsproplem14  28032  precsexlem1  28109  precsexlem2  28110  onsiso  28169  bdayn0sf1o  28259  ax5seglem7  28862  axlowdimlem8  28876  axlowdimlem11  28879  vtxvalsnop  28968  iedgvalsnop  28969  umgrislfupgrlem  29049  usgrexmpledg  29189  usgredgffibi  29251  vdegp1bi  29465  edginwlk  29563  uhgrwkspthlem2  29684  clwwlkvbij  30042  wlk2v2elem2  30085  frgrwopreglem3  30243  ex-dif  30352  ex-xp  30365  ex-rn  30369  ex-lcm  30387  ex-prmo  30388  ip0i  30754  ip1ilem  30755  ipdirilem  30758  ipasslem10  30768  hvnegdii  30991  hvaddcani  30994  hvsubaddi  30995  hisubcomi  31033  normlem0  31038  normlem3  31041  normlem9  31047  bcseqi  31049  norm0  31057  norm-ii-i  31066  norm3difi  31076  normpari  31083  normpar2i  31085  polid2i  31086  shs0i  31378  chj0i  31384  pjsslem  31608  ho0subi  31724  hoaddsubi  31750  hosd1i  31751  hopncani  31753  nmop0  31915  nmfn0  31916  lnopunilem1  31939  lnophmlem2  31946  opsqrlem2  32070  pjclem1  32124  atabsi  32330  dmdbr6ati  32352  inin  32445  iuninc  32489  gtiso  32624  f1od2  32644  fpwrelmapffs  32657  fzodif1  32715  nn0split01  32742  dfdec100  32755  dp20u  32798  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpmul  32833  dpmul4  32834  1mhdrd  32836  cycpmrn  33100  tocyccntz  33101  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  lmat22det  33812  ordtcnvNEW  33910  ordtrest2NEW  33913  zlmtset  33953  qqhucn  33982  esumnul  34038  mbfmcst  34250  carsggect  34309  eulerpartgbij  34363  eulerpartlemn  34372  fib0  34390  fib1  34391  fib2  34393  fib3  34394  fib4  34395  fib5  34396  fib6  34397  0rrv  34442  coinflipprob  34471  ballotlem2  34480  ballotth  34529  signsvf0  34571  itgexpif  34597  hgt750lem  34642  hgt750lem2  34643  bnj1416  35029  derang0  35156  subfac0  35164  subfac1  35165  satfv1  35350  fmla  35368  fmla0  35369  fmla0xp  35370  fmla1  35374  mthmpps  35569  problem2  35653  quad3  35657  dfrdg2  35783  pprodcnveq  35871  dffv5  35912  fullfunfv  35935  ellines  36140  rankeq1o  36159  onint1  36437  bj-xpimasn  36943  bj-pr11val  36993  bj-pr21val  37001  bj-pr22val  37007  bj-nuliotaALT  37046  bj-dfmpoa  37106  bj-opabco  37176  icorempo  37339  finxpreclem4  37382  finxp2o  37387  finxp3o  37388  matunitlindf  37612  poimirlem5  37619  poimirlem22  37636  poimirlem26  37640  poimirlem30  37644  ismblfin  37655  dvtan  37664  asindmre  37697  dvasin  37698  dvacos  37699  areacirclem5  37706  heiborlem6  37810  dmcnvep  38361  dmxrncnvep  38362  xrnres4  38391  dfcoels  38421  coss0  38470  refsymrels2  38556  dfeqvrels2  38579  refrelsredund4  38623  hdmap1cbv  41796  lcm4un  42004  lcm5un  42005  lcm6un  42006  lcm7un  42007  lcm8un  42008  3lexlogpow5ineq1  42042  5bc2eq10  42130  imaopab  42219  decpmul  42276  cxpi11d  42331  tan3rdpi  42340  sin2t3rdpi  42341  cos2t3rdpi  42342  readvrec2  42349  remul02  42393  fltnltalem  42650  sum9cubes  42660  diophrw  42747  dnwech  43037  lmhmlnmsplit  43076  fgraphopab  43192  arearect  43204  areaquad  43205  oaomoencom  43306  dmnonrel  43579  imanonrel  43582  cononrel1  43583  cononrel2  43584  rclexi  43604  rtrclex  43606  dfrtrcl5  43618  sqrtcval  43630  resqrtvalex  43634  imsqrtvalex  43635  cnvtrrel  43659  dfrcl2  43663  dfrcl4  43665  iunrelexp0  43691  comptiunov2i  43695  relexpaddss  43707  brtrclfv2  43716  trclfvdecomr  43717  corcltrcl  43728  cotrclrcl  43731  fsovcnvlem  44002  neicvgnvo  44104  scottabf  44229  mnuprdlem1  44261  hashnzfz  44309  lhe4.4ex1a  44318  tgqioo2  45545  sumnnodd  45628  limsup0  45692  limsup10ex  45771  liminf10ex  45772  cosnegpi  45865  itgsin0pilem1  45948  stoweidlem13  46011  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  dirkertrigeqlem1  46096  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  sqwvfoura  46226  fouriersw  46229  etransclem23  46255  etransclem36  46268  etransclem38  46270  carageniuncllem1  46519  0ome  46527  ovn02  46566  smflimlem4  46772  smflim  46775  smflim2  46804  smflimsup  46826  smfliminf  46829  fmtno0  47541  fmtno1  47542  fmtno2  47551  fmtno3  47552  fmtno4  47553  fmtno5lem4  47557  139prmALT  47597  31prm  47598  5tcu2e40  47616  3exp4mod41  47617  41prothprmlem2  47619  41prothprm  47620  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  tgoldbachlt  47817  isuspgrim0lem  47893  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  usgrexmpl1vtx  48014  usgrexmpl1edg  48015  usgrexmpl2vtx  48019  usgrexmpl2edg  48020  gpg5gricstgr3  48081  gpgprismgr4cycllem7  48091  cznrnglem  48247  2t6m3t4e0  48336  zlmodzxzldeplem3  48491  ackval0  48669  ackval1  48670  ackval2  48671  ackval3  48672  ackval40  48682  ackval42  48685  ackval50  48687  disjdifb  48798  dftpos6  48863  tposresg  48866  tposrescnv  48867  tposres3  48869  tposid  48873  iscnrm3rlem1  48928  dfswapf2  49250  setc1onsubc  49591  sec0  49749