Theorem 3eqtri 2762

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

Syntax hints:   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  csbid  3905  csbconstg  3911  csbie  3928  un23  4167  in32  4220  dfnul4  4323  dfnul2OLD  4326  unvdif  4473  undif2  4475  undifabs  4476  difun2  4479  difdifdir  4490  dfif4  4542  dfif5  4543  tpidm23  4760  dfopif  4869  dfiunv2  5037  symdif0  5087  symdifid  5089  unidif0  5357  uniop  5514  xpun  5748  dfrn2  5887  dfdmf  5895  dfrnf  5948  res0  5984  resres  5993  xpssres  6017  dfima2  6060  imai  6072  ima0  6075  imaundir  6149  xpima  6180  cnvrescnv  6193  dmresv  6198  rescnvcnv  6202  dmtpop  6216  rnsnopg  6219  resdmres  6230  resdifdi  6234  dmmpt  6238  dmco  6252  co01  6259  suc0  6438  iunsuc  6448  fresaun  6761  dffv4  6887  fvssunirnOLD  6924  f1ossf1o  7127  fpr  7153  mpo0  7496  dmoprab  7512  rnoprab  7514  elrnmpores  7548  ov6g  7573  1st0  7983  2nd0  7984  dfmpo  8090  curry1  8092  curry2  8095  fpar  8104  dftpos2  8230  tposoprab  8249  tposmpo  8250  fvmpocurryd  8258  frrlem14  8286  dfwrecsOLD  8300  wfrlem14OLD  8324  wfrlem16OLD  8326  dfrecs3  8374  dfrecs3OLD  8375  tfrlem8  8386  seqomlem3  8454  df2o3  8476  nlim2  8492  omxpenlem  9075  dfsdom2  9098  pwfir  9178  marypha2lem2  9433  sup00  9461  epinid0  9597  scottexs  9884  scott0s  9885  infxpenc2  10019  kmlem3  10149  ackbij1lem2  10218  compsscnv  10368  fin1a2lem12  10408  mulerpqlem  10952  1lt2nq  10970  axi2m1  11156  2p2e4  12351  numsuc  12695  numsucc  12721  decmul10add  12750  5p5e10  12752  6p4e10  12753  7p3e10  12756  xnegmnf  13193  pnfaddmnf  13213  fz12pr  13562  fz0tp  13606  fz0to3un2pr  13607  fzo13pr  13720  fzo0to2pr  13721  fzo0to3tp  13722  fzo0to42pr  13723  fzo1to4tp  13724  fldiv4p1lem1div2  13804  sq4e2t8  14167  i4  14172  crreczi  14195  fac1  14241  fac3  14244  hashkf  14296  hashinf  14299  dmhashres  14305  hashun3  14348  cshwsexaOLD  14779  dmtrclfv  14969  abs0  15236  absi  15237  trirecip  15813  geoihalfsum  15832  esum  16028  tan0  16098  coshval  16102  ef01bndlem  16131  3dvds  16278  3dvdsdec  16279  3dvds2dec  16280  sadc0  16399  3lcm2e6woprm  16556  6lcm4e12  16557  lcmf0  16575  prmo0  16973  gcdmodi  17011  karatsuba  17021  43prm  17059  139prm  17061  631prm  17064  1259lem1  17068  1259lem2  17069  1259lem3  17070  1259lem4  17071  1259lem5  17072  2503lem1  17074  2503lem2  17075  2503lem3  17076  4001lem1  17078  4001lem2  17079  4001lem3  17080  4001lem4  17081  setsfun  17108  setsfun0  17109  ndxarg  17133  pmtrsn  19428  psgnprfval1  19431  sylow2a  19528  ablfac1eu  19984  sralem  20935  sralemOLD  20936  pzriprng1ALT  21265  opsrtoslem2  21836  ply1plusgfvi  21984  pf1rcl  22088  restcld  22896  neitr  22904  txbasval  23330  txindis  23358  cnmpt1st  23392  cnmpt2nd  23393  ufildr  23655  restmetu  24299  cphipval2  24989  reust  25129  ehl0base  25164  ismbl  25275  mbfimaopnlem  25404  itg10  25437  itg2cnlem2  25512  itgz  25530  dvmptid  25709  cos2pi  26222  tan4thpi  26260  sincos6thpi  26261  pige3ALT  26265  dfrelog  26310  logm1  26333  dvlog  26395  efopnlem2  26401  cxpexp  26412  root1id  26498  sqrt2cxp2logb9e3  26540  ang180lem2  26551  1cubrlem  26582  quart1  26597  atandm2  26618  efiasin  26629  asinsinlem  26632  asinsin  26633  asin1  26635  acos1  26636  atancj  26651  atanlogsublem  26656  efiatan2  26658  2efiatan  26659  tanatan  26660  dvatan  26676  log2cnv  26685  log2ublem2  26688  log2ublem3  26689  birthday  26695  basellem8  26828  cht1  26905  chp1  26907  ppi1i  26908  ppi2i  26909  cht2  26912  cht3  26913  bclbnd  27019  bposlem8  27030  2lgslem3c  27137  2lgslem3d  27138  noetasuplem2  27473  noetasuplem3  27474  noetasuplem4  27475  noetainflem4  27479  bday0s  27566  old0  27591  new0  27606  left1s  27626  right1s  27627  sltlpss  27638  slelss  27639  mulsproplem13  27823  mulsproplem14  27824  precsexlem1  27892  precsexlem2  27893  ax5seglem7  28460  axlowdimlem8  28474  axlowdimlem11  28477  vtxvalsnop  28568  iedgvalsnop  28569  umgrislfupgrlem  28649  usgrexmpledg  28786  usgredgffibi  28848  vdegp1bi  29061  edginwlk  29159  uhgrwkspthlem2  29278  clwwlkvbij  29633  wlk2v2elem2  29676  frgrwopreglem3  29834  ex-dif  29943  ex-xp  29956  ex-rn  29960  ex-lcm  29978  ex-prmo  29979  ip0i  30345  ip1ilem  30346  ipdirilem  30349  ipasslem10  30359  hvnegdii  30582  hvaddcani  30585  hvsubaddi  30586  hisubcomi  30624  normlem0  30629  normlem3  30632  normlem9  30638  bcseqi  30640  norm0  30648  norm-ii-i  30657  norm3difi  30667  normpari  30674  normpar2i  30676  polid2i  30677  shs0i  30969  chj0i  30975  pjsslem  31199  ho0subi  31315  hoaddsubi  31341  hosd1i  31342  hopncani  31344  nmop0  31506  nmfn0  31507  lnopunilem1  31530  lnophmlem2  31537  opsqrlem2  31661  pjclem1  31715  atabsi  31921  dmdbr6ati  31943  inin  32020  iuninc  32059  gtiso  32189  f1od2  32213  fpwrelmapffs  32226  fzodif1  32271  dfdec100  32303  dp20u  32311  dp3mul10  32331  dpmul1000  32332  dpexpp1  32341  dpadd2  32343  dpmul  32346  dpmul4  32347  1mhdrd  32349  cycpmrn  32572  tocyccntz  32573  lmat22det  33100  ordtcnvNEW  33198  ordtrest2NEW  33201  zlmtset  33242  zlmtsetOLD  33243  qqhucn  33270  esumnul  33344  mbfmcst  33556  carsggect  33615  eulerpartgbij  33669  eulerpartlemn  33678  fib0  33696  fib1  33697  fib2  33699  fib3  33700  fib4  33701  fib5  33702  fib6  33703  0rrv  33748  coinflipprob  33776  ballotlem2  33785  ballotth  33834  signsvf0  33889  itgexpif  33916  hgt750lem  33961  hgt750lem2  33962  bnj1416  34348  derang0  34458  subfac0  34466  subfac1  34467  satfv1  34652  fmla  34670  fmla0  34671  fmla0xp  34672  fmla1  34676  mthmpps  34871  problem2  34949  quad3  34953  dfrdg2  35071  pprodcnveq  35159  dffv5  35200  fullfunfv  35223  ellines  35428  rankeq1o  35447  onint1  35637  bj-xpimasn  36139  bj-pr11val  36189  bj-pr21val  36197  bj-pr22val  36203  bj-nuliotaALT  36242  bj-dfmpoa  36302  bj-opabco  36372  icorempo  36535  finxpreclem4  36578  finxp2o  36583  finxp3o  36584  matunitlindf  36789  poimirlem5  36796  poimirlem22  36813  poimirlem26  36817  poimirlem30  36821  ismblfin  36832  dvtan  36841  asindmre  36874  dvasin  36875  dvacos  36876  areacirclem5  36883  heiborlem6  36987  xrnres4  37578  dfcoels  37603  coss0  37652  refsymrels2  37738  dfeqvrels2  37761  refrelsredund4  37805  hdmap1cbv  40976  lcm4un  41187  lcm5un  41188  lcm6un  41189  lcm7un  41190  lcm8un  41191  3lexlogpow5ineq1  41225  5bc2eq10  41264  2xp3dxp2ge1d  41328  imaopab  41356  decpmul  41502  remul02  41580  fltnltalem  41706  sum9cubes  41716  diophrw  41799  dnwech  42092  lmhmlnmsplit  42131  fgraphopab  42254  arearect  42266  areaquad  42267  oaomoencom  42369  dmnonrel  42643  imanonrel  42646  cononrel1  42647  cononrel2  42648  rclexi  42668  rtrclex  42670  dfrtrcl5  42682  sqrtcval  42694  resqrtvalex  42698  imsqrtvalex  42699  cnvtrrel  42723  dfrcl2  42727  dfrcl4  42729  iunrelexp0  42755  comptiunov2i  42759  relexpaddss  42771  brtrclfv2  42780  trclfvdecomr  42781  corcltrcl  42792  cotrclrcl  42795  fsovcnvlem  43066  neicvgnvo  43168  scottabf  43301  mnuprdlem1  43333  hashnzfz  43381  lhe4.4ex1a  43390  tgqioo2  44558  sumnnodd  44644  limsup0  44708  limsup10ex  44787  liminf10ex  44788  cosnegpi  44881  itgsin0pilem1  44964  stoweidlem13  45027  wallispilem4  45082  wallispi2lem1  45085  wallispi2lem2  45086  stirlinglem3  45090  dirkertrigeqlem1  45112  fourierdlem56  45176  fourierdlem57  45177  fourierdlem58  45178  fourierdlem62  45182  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  sqwvfoura  45242  fouriersw  45245  etransclem23  45271  etransclem36  45284  etransclem38  45286  carageniuncllem1  45535  0ome  45543  ovn02  45582  smflimlem4  45788  smflim  45791  smflim2  45820  smflimsup  45842  smfliminf  45845  fmtno0  46506  fmtno1  46507  fmtno2  46516  fmtno3  46517  fmtno4  46518  fmtno5lem4  46522  139prmALT  46562  31prm  46563  5tcu2e40  46581  3exp4mod41  46582  41prothprmlem2  46584  41prothprm  46585  nnsum3primesgbe  46758  nnsum4primesodd  46762  nnsum4primesoddALTV  46763  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  bgoldbtbndlem1  46771  tgoldbachlt  46782  cznrnglem  46939  2t6m3t4e0  47112  zlmodzxzldeplem3  47270  ackval0  47453  ackval1  47454  ackval2  47455  ackval3  47456  ackval40  47466  ackval42  47469  ackval50  47471  disjdifb  47581  iscnrm3rlem1  47660  mndtchom  47797  sec0  47892