Theorem 3eqtri 2767

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 2763	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2763	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 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-9 2113  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1779  df-cleq 2727

This theorem is referenced by:  csbid  3849  csbconstg  3855  csbie  3872  un23  4107  in32  4160  dfnul4  4263  dfnul2OLD  4266  unvdif  4413  undif2  4415  undifabs  4416  difun2  4419  difdifdir  4427  dfif4  4479  dfif5  4480  tpidm23  4696  dfopif  4805  dfiunv2  4971  symdif0  5020  symdifid  5022  unidif0  5290  uniop  5441  xpun  5671  dfrn2  5810  dfdmf  5818  dfrnf  5871  res0  5907  resres  5916  xpssres  5940  dfima2  5981  imai  5992  ima0  5995  imaundir  6069  xpima  6100  cnvrescnv  6113  dmresv  6118  rescnvcnv  6122  dmtpop  6136  rnsnopg  6139  resdmres  6150  resdifdi  6154  dmmpt  6158  dmco  6172  co01  6179  suc0  6355  iunsuc  6365  fresaun  6675  dffv4  6801  fvssunirn  6835  f1ossf1o  7032  fpr  7058  mpo0  7393  dmoprab  7409  rnoprab  7411  elrnmpores  7444  ov6g  7469  1st0  7873  2nd0  7874  dfmpo  7978  curry1  7980  curry2  7983  fpar  7992  dftpos2  8094  tposoprab  8113  tposmpo  8114  fvmpocurryd  8122  frrlem14  8150  dfwrecsOLD  8164  wfrlem14OLD  8188  wfrlem16OLD  8190  dfrecs3  8238  dfrecs3OLD  8239  tfrlem8  8250  seqomlem3  8318  df2o3  8340  nlim2  8356  omxpenlem  8903  dfsdom2  8926  pwfir  9006  marypha2lem2  9253  sup00  9281  epinid0  9417  scottexs  9703  scott0s  9704  infxpenc2  9838  kmlem3  9968  ackbij1lem2  10037  compsscnv  10187  fin1a2lem12  10227  mulerpqlem  10771  1lt2nq  10789  axi2m1  10975  2p2e4  12168  numsuc  12511  numsucc  12537  decmul10add  12566  5p5e10  12568  6p4e10  12569  7p3e10  12572  xnegmnf  13004  pnfaddmnf  13024  fz12pr  13373  fz0tp  13417  fz0to3un2pr  13418  fzo13pr  13531  fzo0to2pr  13532  fzo0to3tp  13533  fzo0to42pr  13534  fzo1to4tp  13535  fldiv4p1lem1div2  13615  sq4e2t8  13976  i4  13981  crreczi  14003  fac1  14051  fac3  14054  hashkf  14106  hashinf  14109  dmhashres  14115  hashun3  14158  cshwsexa  14596  dmtrclfv  14788  abs0  15056  absi  15057  trirecip  15634  geoihalfsum  15653  esum  15849  tan0  15919  coshval  15923  ef01bndlem  15952  3dvds  16099  3dvdsdec  16100  3dvds2dec  16101  sadc0  16220  3lcm2e6woprm  16379  6lcm4e12  16380  lcmf0  16398  prmo0  16796  gcdmodi  16834  karatsuba  16844  43prm  16882  139prm  16884  631prm  16887  1259lem1  16891  1259lem2  16892  1259lem3  16893  1259lem4  16894  1259lem5  16895  2503lem1  16897  2503lem2  16898  2503lem3  16899  4001lem1  16901  4001lem2  16902  4001lem3  16903  4001lem4  16904  setsfun  16931  setsfun0  16932  ndxarg  16956  pmtrsn  19186  psgnprfval1  19189  sylow2a  19283  ablfac1eu  19735  sralem  20502  sralemOLD  20503  opsrtoslem2  21326  ply1plusgfvi  21476  pf1rcl  21578  restcld  22386  neitr  22394  txbasval  22820  txindis  22848  cnmpt1st  22882  cnmpt2nd  22883  ufildr  23145  restmetu  23789  cphipval2  24468  reust  24608  ehl0base  24643  ismbl  24753  mbfimaopnlem  24882  itg10  24915  itg2cnlem2  24990  itgz  25008  dvmptid  25184  cos2pi  25696  tan4thpi  25734  sincos6thpi  25735  pige3ALT  25739  dfrelog  25784  logm1  25807  dvlog  25869  efopnlem2  25875  cxpexp  25886  root1id  25970  sqrt2cxp2logb9e3  26012  ang180lem2  26023  1cubrlem  26054  quart1  26069  atandm2  26090  efiasin  26101  asinsinlem  26104  asinsin  26105  asin1  26107  acos1  26108  atancj  26123  atanlogsublem  26128  efiatan2  26130  2efiatan  26131  tanatan  26132  dvatan  26148  log2cnv  26157  log2ublem2  26160  log2ublem3  26161  birthday  26167  basellem8  26300  cht1  26377  chp1  26379  ppi1i  26380  ppi2i  26381  cht2  26384  cht3  26385  bclbnd  26491  bposlem8  26502  2lgslem3c  26609  2lgslem3d  26610  ax5seglem7  27401  axlowdimlem8  27415  axlowdimlem11  27418  vtxvalsnop  27509  iedgvalsnop  27510  umgrislfupgrlem  27590  usgrexmpledg  27727  usgredgffibi  27789  vdegp1bi  28002  edginwlk  28100  uhgrwkspthlem2  28220  clwwlkvbij  28575  wlk2v2elem2  28618  frgrwopreglem3  28776  ex-dif  28885  ex-xp  28898  ex-rn  28902  ex-lcm  28920  ex-prmo  28921  ip0i  29285  ip1ilem  29286  ipdirilem  29289  ipasslem10  29299  hvnegdii  29522  hvaddcani  29525  hvsubaddi  29526  hisubcomi  29564  normlem0  29569  normlem3  29572  normlem9  29578  bcseqi  29580  norm0  29588  norm-ii-i  29597  norm3difi  29607  normpari  29614  normpar2i  29616  polid2i  29617  shs0i  29909  chj0i  29915  pjsslem  30139  ho0subi  30255  hoaddsubi  30281  hosd1i  30282  hopncani  30284  nmop0  30446  nmfn0  30447  lnopunilem1  30470  lnophmlem2  30477  opsqrlem2  30601  pjclem1  30655  atabsi  30861  dmdbr6ati  30883  inin  30960  iuninc  30998  gtiso  31131  f1od2  31154  fpwrelmapffs  31167  fzodif1  31212  dfdec100  31242  dp20u  31250  dp3mul10  31270  dpmul1000  31271  dpexpp1  31280  dpadd2  31282  dpmul  31285  dpmul4  31286  1mhdrd  31288  cycpmrn  31508  tocyccntz  31509  lmat22det  31868  ordtcnvNEW  31966  ordtrest2NEW  31969  zlmtset  32010  zlmtsetOLD  32011  qqhucn  32038  esumnul  32112  mbfmcst  32322  carsggect  32381  eulerpartgbij  32435  eulerpartlemn  32444  fib0  32462  fib1  32463  fib2  32465  fib3  32466  fib4  32467  fib5  32468  fib6  32469  0rrv  32514  coinflipprob  32542  ballotlem2  32551  ballotth  32600  signsvf0  32655  itgexpif  32682  hgt750lem  32727  hgt750lem2  32728  bnj1416  33115  derang0  33227  subfac0  33235  subfac1  33236  satfv1  33421  fmla  33439  fmla0  33440  fmla0xp  33441  fmla1  33445  mthmpps  33640  problem2  33720  quad3  33724  dfrdg2  33865  noetasuplem2  33996  noetasuplem3  33997  noetasuplem4  33998  noetainflem4  34002  bday0s  34081  old0  34102  new0  34117  sltlpss  34146  pprodcnveq  34244  dffv5  34285  fullfunfv  34308  ellines  34513  rankeq1o  34532  onint1  34697  bj-xpimasn  35203  bj-pr11val  35253  bj-pr21val  35261  bj-pr22val  35267  bj-nuliotaALT  35287  bj-dfmpoa  35347  bj-opabco  35417  icorempo  35580  finxpreclem4  35623  finxp2o  35628  finxp3o  35629  matunitlindf  35833  poimirlem5  35840  poimirlem22  35857  poimirlem26  35861  poimirlem30  35865  ismblfin  35876  dvtan  35885  asindmre  35918  dvasin  35919  dvacos  35920  areacirclem5  35927  heiborlem6  36032  xrnres4  36629  dfcoels  36654  coss0  36703  refsymrels2  36789  dfeqvrels2  36812  refrelsredund4  36856  hdmap1cbv  40026  lcm4un  40234  lcm5un  40235  lcm6un  40236  lcm7un  40237  lcm8un  40238  3lexlogpow5ineq1  40272  5bc2eq10  40311  2xp3dxp2ge1d  40375  imaopab  40415  sqn5ii  40522  decpmul  40524  remul02  40596  rei4  40613  sn-0lt1  40640  fltnltalem  40707  diophrw  40789  dnwech  41082  lmhmlnmsplit  41121  fgraphopab  41244  arearect  41255  areaquad  41256  dmnonrel  41424  imanonrel  41427  cononrel1  41428  cononrel2  41429  rclexi  41449  rtrclex  41451  dfrtrcl5  41463  sqrtcval  41475  resqrtvalex  41479  imsqrtvalex  41480  cnvtrrel  41504  dfrcl2  41508  dfrcl4  41510  iunrelexp0  41536  comptiunov2i  41540  relexpaddss  41552  brtrclfv2  41561  trclfvdecomr  41562  corcltrcl  41573  cotrclrcl  41576  fsovcnvlem  41847  neicvgnvo  41951  scottabf  42084  mnuprdlem1  42116  hashnzfz  42164  lhe4.4ex1a  42173  tgqioo2  43327  sumnnodd  43413  limsup0  43477  limsup10ex  43556  liminf10ex  43557  cosnegpi  43650  itgsin0pilem1  43733  stoweidlem13  43796  wallispilem4  43851  wallispi2lem1  43854  wallispi2lem2  43855  stirlinglem3  43859  dirkertrigeqlem1  43881  fourierdlem56  43945  fourierdlem57  43946  fourierdlem58  43947  fourierdlem62  43951  fourierdlem103  43992  fourierdlem104  43993  fourierdlem112  44001  sqwvfoura  44011  fouriersw  44014  etransclem23  44040  etransclem36  44053  etransclem38  44055  carageniuncllem1  44302  0ome  44310  ovn02  44349  smflimlem4  44555  smflim  44558  smflim2  44587  smflimsup  44609  smfliminf  44612  fmtno0  45249  fmtno1  45250  fmtno2  45259  fmtno3  45260  fmtno4  45261  fmtno5lem4  45265  139prmALT  45305  31prm  45306  5tcu2e40  45324  3exp4mod41  45325  41prothprmlem2  45327  41prothprm  45328  nnsum3primesgbe  45501  nnsum4primesodd  45505  nnsum4primesoddALTV  45506  nnsum4primeseven  45509  nnsum4primesevenALTV  45510  bgoldbtbndlem1  45514  tgoldbachlt  45525  cznrnglem  45768  2t6m3t4e0  45941  zlmodzxzldeplem3  46100  ackval0  46283  ackval1  46284  ackval2  46285  ackval3  46286  ackval40  46296  ackval42  46299  ackval50  46301  disjdifb  46412  iscnrm3rlem1  46491  mndtchom  46628  sec0  46719