Theorem 3eqtri 2766

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

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  csbid  3844  csbconstg  3850  csbie  3866  un23  4103  in32  4158  dfnul4  4263  unvdif  4403  undif2  4405  undifabs  4406  difun2  4409  difdifdir  4419  dfif4  4470  dfif5  4471  tpidm23  4689  dfopif  4801  dfiunv2  4963  symdif0  5014  symdifv  5015  symdifid  5016  unidif0  5288  unidif0OLD  5289  uniop  5456  xpun  5692  dfrn2  5830  dfdmf  5838  dfrnf  5892  res0  5935  resres  5944  xpssres  5970  dfima2  6014  imai  6026  ima0  6029  imaundir  6101  xpima  6133  cnvrescnv  6146  dmresv  6151  rescnvcnv  6155  dmtpop  6169  rnsnopg  6172  resdmres  6183  resdifdi  6187  dmmpt  6191  dmco  6206  co01  6213  suc0  6387  iunsuc  6397  fresaun  6698  dffv4  6824  f1ossf1o  7070  fpr  7097  mpo0  7441  dmoprab  7459  rnoprab  7461  elrnmpores  7494  ov6g  7520  1st0  7937  2nd0  7938  dfmpo  8041  curry1  8043  curry2  8046  fpar  8055  dftpos2  8183  tposoprab  8202  tposmpo  8203  fvmpocurryd  8211  frrlem14  8239  dfrecs3  8302  tfrlem8  8313  seqomlem3  8381  df2o3  8403  nlim2  8415  omxpenlem  9006  dfsdom2  9028  pwfir  9217  marypha2lem2  9339  sup00  9368  epinid0  9510  scottexs  9802  scott0s  9803  infxpenc2  9935  kmlem3  10066  ackbij1lem2  10133  compsscnv  10284  fin1a2lem12  10324  mulerpqlem  10869  1lt2nq  10887  axi2m1  11073  2p2e4  12302  numsuc  12649  numsucc  12675  decmul10add  12704  5p5e10  12706  6p4e10  12707  7p3e10  12710  xnegmnf  13153  pnfaddmnf  13173  fz12pr  13526  fz0tp  13573  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  fzo13pr  13695  fzo0to2pr  13696  fz01pr  13697  fzo0to3tp  13698  fzo0to42pr  13699  fzo1to4tp  13700  fldiv4p1lem1div2  13785  sq4e2t8  14152  i4  14157  crreczi  14181  fac1  14230  fac3  14233  hashkf  14285  hashinf  14288  dmhashres  14294  hashun3  14337  dmtrclfv  14971  abs0  15238  absi  15239  trirecip  15819  geoihalfsum  15838  esum  16036  tan0  16109  coshval  16113  ef01bndlem  16142  3dvds  16291  3dvdsdec  16292  3dvds2dec  16293  sadc0  16414  3lcm2e6woprm  16575  6lcm4e12  16576  lcmf0  16594  prmo0  16998  gcdmodi  17036  karatsuba  17045  43prm  17083  139prm  17085  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  setsfun  17132  setsfun0  17133  ndxarg  17157  chnccat  18583  ex-chn2  18595  pmtrsn  19485  psgnprfval1  19488  sylow2a  19585  ablfac1eu  20041  sralem  21166  pzriprng1ALT  21471  opsrtoslem2  22032  ply1plusgfvi  22226  pf1rcl  22335  restcld  23155  neitr  23163  txbasval  23589  txindis  23617  cnmpt1st  23651  cnmpt2nd  23652  ufildr  23914  restmetu  24553  cphipval2  25226  reust  25366  ehl0base  25401  ismbl  25511  mbfimaopnlem  25640  itg10  25673  itg2cnlem2  25747  itgz  25766  dvmptid  25942  cos2pi  26458  tan4thpi  26496  tan4thpiOLD  26497  sincos6thpi  26498  pige3ALT  26502  dfrelog  26547  logm1  26571  dvlog  26633  efopnlem2  26639  cxpexp  26650  root1id  26736  sqrt2cxp2logb9e3  26781  ang180lem2  26792  1cubrlem  26823  quart1  26838  atandm2  26859  efiasin  26870  asinsinlem  26873  asinsin  26874  asin1  26876  acos1  26877  atancj  26892  atanlogsublem  26897  efiatan2  26899  2efiatan  26900  tanatan  26901  dvatan  26917  log2cnv  26926  log2ublem2  26929  log2ublem3  26930  birthday  26936  basellem8  27069  cht1  27146  chp1  27148  ppi1i  27149  ppi2i  27150  cht2  27153  cht3  27154  bclbnd  27261  bposlem8  27272  2lgslem3c  27379  2lgslem3d  27380  noetasuplem2  27716  noetasuplem3  27717  noetasuplem4  27718  noetainflem4  27722  bday0  27821  old0  27849  new0  27874  left1s  27905  right1s  27906  ltslpss  27918  leslss  27919  mulsproplem13  28138  mulsproplem14  28139  precsexlem1  28217  precsexlem2  28218  oniso  28281  bdayn0sf1o  28380  ax5seglem7  29022  axlowdimlem8  29036  axlowdimlem11  29039  vtxvalsnop  29128  iedgvalsnop  29129  umgrislfupgrlem  29209  usgrexmpledg  29349  usgredgffibi  29411  vdegp1bi  29624  edginwlk  29721  uhgrwkspthlem2  29840  clwwlkvbij  30201  wlk2v2elem2  30244  frgrwopreglem3  30402  ex-dif  30511  ex-xp  30524  ex-rn  30528  ex-lcm  30546  ex-prmo  30547  ip0i  30914  ip1ilem  30915  ipdirilem  30918  ipasslem10  30928  hvnegdii  31151  hvaddcani  31154  hvsubaddi  31155  hisubcomi  31193  normlem0  31198  normlem3  31201  normlem9  31207  bcseqi  31209  norm0  31217  norm-ii-i  31226  norm3difi  31236  normpari  31243  normpar2i  31245  polid2i  31246  shs0i  31538  chj0i  31544  pjsslem  31768  ho0subi  31884  hoaddsubi  31910  hosd1i  31911  hopncani  31913  nmop0  32075  nmfn0  32076  lnopunilem1  32099  lnophmlem2  32106  opsqrlem2  32230  pjclem1  32284  atabsi  32490  dmdbr6ati  32512  inin  32604  iuninc  32649  gtiso  32793  f1od2  32811  fpwrelmapffs  32826  fzodif1  32884  nn0split01  32910  dfdec100  32922  dp20u  32956  dp3mul10  32976  dpmul1000  32977  dpexpp1  32986  dpadd2  32988  dpmul  32991  dpmul4  32992  1mhdrd  32994  cycpmrn  33224  tocyccntz  33225  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  lmat22det  34006  ordtcnvNEW  34104  ordtrest2NEW  34107  zlmtset  34147  qqhucn  34176  esumnul  34232  mbfmcst  34443  carsggect  34502  eulerpartgbij  34556  eulerpartlemn  34565  fib0  34583  fib1  34584  fib2  34586  fib3  34587  fib4  34588  fib5  34589  fib6  34590  0rrv  34635  coinflipprob  34664  ballotlem2  34673  ballotth  34722  signsvf0  34764  itgexpif  34790  hgt750lem  34835  hgt750lem2  34836  bnj1416  35221  r11  35275  r12  35276  derang0  35397  subfac0  35405  subfac1  35406  satfv1  35591  fmla  35609  fmla0  35610  fmla0xp  35611  fmla1  35615  mthmpps  35810  problem2  35894  quad3  35898  dfrdg2  36021  pprodcnveq  36109  dffv5  36150  dfsuccf2  36169  fullfunfv  36175  ellines  36380  rankeq1o  36399  onint1  36677  bj-xpimasn  37308  bj-pr11val  37358  bj-pr21val  37366  bj-pr22val  37372  bj-nuliotaALT  37411  bj-dfmpoa  37476  bj-opabco  37548  icorempo  37713  finxpreclem4  37756  finxp2o  37761  finxp3o  37762  matunitlindf  37985  poimirlem5  37992  poimirlem22  38009  poimirlem26  38013  poimirlem30  38017  ismblfin  38028  dvtan  38037  asindmre  38070  dvasin  38071  dvacos  38072  areacirclem5  38079  heiborlem6  38183  dmcnvep  38755  dmxrncnvep  38756  dmcnvepres  38757  dmxrnuncnvepres  38759  xrnres4  38795  dfadjliftmap2  38824  blockadjliftmap  38825  dfblockliftmap2  38828  dfsucmap3  38830  dfsuccl2  38837  dfcoels  38887  coss0  38936  refsymrels2  39016  dfeqvrels2  39039  refrelsredund4  39083  hdmap1cbv  42294  lcm4un  42501  lcm5un  42502  lcm6un  42503  lcm7un  42504  lcm8un  42505  3lexlogpow5ineq1  42539  5bc2eq10  42627  imaopab  42718  decpmul  42765  cxpi11d  42820  tan3rdpi  42829  sin2t3rdpi  42830  cos2t3rdpi  42831  readvrec2  42838  remul02  42882  fltnltalem  43112  sum9cubes  43122  diophrw  43208  dnwech  43493  lmhmlnmsplit  43532  fgraphopab  43648  arearect  43660  areaquad  43661  oaomoencom  43762  dmnonrel  44034  imanonrel  44037  cononrel1  44038  cononrel2  44039  rclexi  44059  rtrclex  44061  dfrtrcl5  44073  sqrtcval  44085  resqrtvalex  44089  imsqrtvalex  44090  cnvtrrel  44114  dfrcl2  44118  dfrcl4  44120  iunrelexp0  44146  comptiunov2i  44150  relexpaddss  44162  brtrclfv2  44171  trclfvdecomr  44172  corcltrcl  44183  cotrclrcl  44186  fsovcnvlem  44457  neicvgnvo  44559  scottabf  44684  mnuprdlem1  44716  hashnzfz  44764  lhe4.4ex1a  44773  tgqioo2  45992  sumnnodd  46075  limsup0  46137  limsup10ex  46216  liminf10ex  46217  cosnegpi  46310  itgsin0pilem1  46393  stoweidlem13  46456  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem3  46519  dirkertrigeqlem1  46541  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  sqwvfoura  46671  fouriersw  46674  etransclem23  46700  etransclem36  46713  etransclem38  46715  carageniuncllem1  46964  0ome  46972  ovn02  47011  smflimlem4  47217  smflim  47220  smflim2  47249  smflimsup  47271  smfliminf  47274  cos5t  47342  goldratmolem2  47349  fmtno0  48018  fmtno1  48019  fmtno2  48028  fmtno3  48029  fmtno4  48030  fmtno5lem4  48034  139prmALT  48074  31prm  48075  5tcu2e40  48093  3exp4mod41  48094  41prothprmlem2  48096  41prothprm  48097  ppivalnn4  48105  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  tgoldbachlt  48307  isuspgrim0lem  48384  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  usgrexmpl1vtx  48514  usgrexmpl1edg  48515  usgrexmpl2vtx  48519  usgrexmpl2edg  48520  gpg5gricstgr3  48581  gpgprismgr4cycllem7  48592  cznrnglem  48750  2t6m3t4e0  48839  zlmodzxzldeplem3  48993  ackval0  49171  ackval1  49172  ackval2  49173  ackval3  49174  ackval40  49184  ackval42  49187  ackval50  49189  disjdifb  49300  dftpos6  49365  tposresg  49368  tposrescnv  49369  tposres3  49371  tposid  49375  iscnrm3rlem1  49430  dfswapf2  49751  setc1onsubc  50092  sec0  50250