Theorem 3eqtri 2771

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

Syntax hints:   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731

This theorem is referenced by:  csbid  3842  csbconstg  3848  csbie  3865  un23  4099  in32  4153  dfnul4  4256  dfnul2OLD  4259  unvdif  4406  undif2  4408  undifabs  4409  difun2  4412  difdifdir  4420  dfif4  4471  dfif5  4472  tpidm23  4690  dfopifOLD  4798  dfiunv2  4961  symdif0  5010  symdifid  5012  unidif0  5275  uniop  5422  xpun  5650  dfrn2  5785  dfdmf  5793  dfrnf  5847  res0  5883  resres  5892  xpssres  5916  dfima2  5959  imai  5970  ima0  5973  imaundir  6042  xpima  6073  cnvrescnv  6086  dmresv  6091  rescnvcnv  6095  dmtpop  6109  rnsnopg  6112  resdmres  6123  resdifdi  6127  dmmpt  6131  dmco  6146  co01  6153  suc0  6322  unisuc  6324  iunsuc  6330  fresaun  6626  dffv4  6750  fvssunirn  6782  f1ossf1o  6979  fpr  7005  mpo0  7335  dmoprab  7351  rnoprab  7353  elrnmpores  7386  ov6g  7411  1st0  7807  2nd0  7808  dfmpo  7910  curry1  7912  curry2  7915  fpar  7924  dftpos2  8027  tposoprab  8046  tposmpo  8047  fvmpocurryd  8055  frrlem14  8082  wfrlem14  8110  wfrlem16  8112  dfrecs3  8151  tfrlem8  8162  seqomlem3  8230  df2o3  8259  omxpenlem  8790  dfsdom2  8813  pwfir  8898  marypha2lem2  9100  sup00  9128  epinid0  9264  trpred0  9385  scottexs  9551  scott0s  9552  infxpenc2  9684  kmlem3  9814  ackbij1lem2  9883  compsscnv  10033  fin1a2lem12  10073  mulerpqlem  10617  1lt2nq  10635  axi2m1  10821  2p2e4  12013  numsuc  12355  numsucc  12381  decmul10add  12410  5p5e10  12412  6p4e10  12413  7p3e10  12416  xnegmnf  12848  pnfaddmnf  12868  fz12pr  13217  fz0tp  13261  fz0to3un2pr  13262  fzo13pr  13374  fzo0to2pr  13375  fzo0to3tp  13376  fzo0to42pr  13377  fzo1to4tp  13378  fldiv4p1lem1div2  13458  sq4e2t8  13819  i4  13824  crreczi  13846  fac1  13894  fac3  13897  hashkf  13949  hashinf  13952  dmhashres  13958  hashun3  14002  cshwsexa  14440  dmtrclfv  14632  abs0  14900  absi  14901  trirecip  15478  geoihalfsum  15497  esum  15693  tan0  15763  coshval  15767  ef01bndlem  15796  3dvds  15943  3dvdsdec  15944  3dvds2dec  15945  sadc0  16064  3lcm2e6woprm  16223  6lcm4e12  16224  lcmf0  16242  prmo0  16640  gcdmodi  16678  karatsuba  16688  43prm  16726  139prm  16728  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  setsfun  16775  setsfun0  16776  ndxarg  16800  pmtrsn  19017  psgnprfval1  19020  sylow2a  19114  ablfac1eu  19566  sralem  20329  sralemOLD  20330  opsrtoslem2  21148  ply1plusgfvi  21298  pf1rcl  21400  restcld  22206  neitr  22214  txbasval  22640  txindis  22668  cnmpt1st  22702  cnmpt2nd  22703  ufildr  22965  restmetu  23607  cphipval2  24285  reust  24425  ehl0base  24460  ismbl  24570  mbfimaopnlem  24699  itg10  24732  itg2cnlem2  24807  itgz  24825  dvmptid  25001  cos2pi  25513  tan4thpi  25551  sincos6thpi  25552  pige3ALT  25556  dfrelog  25601  logm1  25624  dvlog  25686  efopnlem2  25692  cxpexp  25703  root1id  25787  sqrt2cxp2logb9e3  25829  ang180lem2  25840  1cubrlem  25871  quart1  25886  atandm2  25907  efiasin  25918  asinsinlem  25921  asinsin  25922  asin1  25924  acos1  25925  atancj  25940  atanlogsublem  25945  efiatan2  25947  2efiatan  25948  tanatan  25949  dvatan  25965  log2cnv  25974  log2ublem2  25977  log2ublem3  25978  birthday  25984  basellem8  26117  cht1  26194  chp1  26196  ppi1i  26197  ppi2i  26198  cht2  26201  cht3  26202  bclbnd  26308  bposlem8  26319  2lgslem3c  26426  2lgslem3d  26427  ax5seglem7  27181  axlowdimlem8  27195  axlowdimlem11  27198  vtxvalsnop  27289  iedgvalsnop  27290  umgrislfupgrlem  27370  usgrexmpledg  27507  usgredgffibi  27569  vdegp1bi  27782  edginwlk  27879  uhgrwkspthlem2  27998  clwwlkvbij  28353  wlk2v2elem2  28396  frgrwopreglem3  28554  ex-dif  28663  ex-xp  28676  ex-rn  28680  ex-lcm  28698  ex-prmo  28699  ip0i  29063  ip1ilem  29064  ipdirilem  29067  ipasslem10  29077  hvnegdii  29300  hvaddcani  29303  hvsubaddi  29304  hisubcomi  29342  normlem0  29347  normlem3  29350  normlem9  29356  bcseqi  29358  norm0  29366  norm-ii-i  29375  norm3difi  29385  normpari  29392  normpar2i  29394  polid2i  29395  shs0i  29687  chj0i  29693  pjsslem  29917  ho0subi  30033  hoaddsubi  30059  hosd1i  30060  hopncani  30062  nmop0  30224  nmfn0  30225  lnopunilem1  30248  lnophmlem2  30255  opsqrlem2  30379  pjclem1  30433  atabsi  30639  dmdbr6ati  30661  inin  30738  iuninc  30776  gtiso  30910  f1od2  30933  fpwrelmapffs  30946  fzodif1  30991  dfdec100  31021  dp20u  31029  dp3mul10  31049  dpmul1000  31050  dpexpp1  31059  dpadd2  31061  dpmul  31064  dpmul4  31065  1mhdrd  31067  cycpmrn  31287  tocyccntz  31288  lmat22det  31649  ordtcnvNEW  31747  ordtrest2NEW  31750  zlmtset  31790  qqhucn  31817  esumnul  31891  mbfmcst  32101  carsggect  32160  eulerpartgbij  32214  eulerpartlemn  32223  fib0  32241  fib1  32242  fib2  32244  fib3  32245  fib4  32246  fib5  32247  fib6  32248  0rrv  32293  coinflipprob  32321  ballotlem2  32330  ballotth  32379  signsvf0  32434  itgexpif  32461  hgt750lem  32506  hgt750lem2  32507  bnj1416  32894  derang0  33006  subfac0  33014  subfac1  33015  satfv1  33200  fmla  33218  fmla0  33219  fmla0xp  33220  fmla1  33224  mthmpps  33419  problem2  33499  quad3  33503  dfrdg2  33652  noetasuplem2  33839  noetasuplem3  33840  noetasuplem4  33841  noetainflem4  33845  bday0s  33924  old0  33945  new0  33960  sltlpss  33989  pprodcnveq  34087  dffv5  34128  fullfunfv  34151  ellines  34356  rankeq1o  34375  onint1  34540  bj-xpimasn  35047  bj-pr11val  35097  bj-pr21val  35105  bj-pr22val  35111  bj-nuliotaALT  35131  bj-dfmpoa  35192  bj-opabco  35262  icorempo  35428  finxpreclem4  35471  finxp2o  35476  finxp3o  35477  matunitlindf  35681  poimirlem5  35688  poimirlem22  35705  poimirlem26  35709  poimirlem30  35713  ismblfin  35724  dvtan  35733  asindmre  35766  dvasin  35767  dvacos  35768  areacirclem5  35775  heiborlem6  35880  xrnres4  36437  dfcoels  36459  coss0  36503  refsymrels2  36585  dfeqvrels2  36607  refrelsredund4  36651  hdmap1cbv  39722  lcm4un  39931  lcm5un  39932  lcm6un  39933  lcm7un  39934  lcm8un  39935  3lexlogpow5ineq1  39969  5bc2eq10  39998  2xp3dxp2ge1d  40062  imaopab  40105  sqn5ii  40207  decpmul  40209  remul02  40281  rei4  40298  sn-0lt1  40325  fltnltalem  40387  diophrw  40469  dnwech  40761  lmhmlnmsplit  40800  fgraphopab  40923  arearect  40934  areaquad  40935  dmnonrel  41059  imanonrel  41062  cononrel1  41063  cononrel2  41064  rclexi  41084  rtrclex  41086  dfrtrcl5  41098  sqrtcval  41110  resqrtvalex  41114  imsqrtvalex  41115  cnvtrrel  41140  dfrcl2  41144  dfrcl4  41146  iunrelexp0  41172  comptiunov2i  41176  relexpaddss  41188  brtrclfv2  41197  trclfvdecomr  41198  corcltrcl  41209  cotrclrcl  41212  fsovcnvlem  41483  neicvgnvo  41587  scottabf  41720  mnuprdlem1  41752  hashnzfz  41800  lhe4.4ex1a  41809  tgqioo2  42948  sumnnodd  43034  limsup0  43098  limsup10ex  43177  liminf10ex  43178  cosnegpi  43271  itgsin0pilem1  43354  stoweidlem13  43417  wallispilem4  43472  wallispi2lem1  43475  wallispi2lem2  43476  stirlinglem3  43480  dirkertrigeqlem1  43502  fourierdlem56  43566  fourierdlem57  43567  fourierdlem58  43568  fourierdlem62  43572  fourierdlem103  43613  fourierdlem104  43614  fourierdlem112  43622  sqwvfoura  43632  fouriersw  43635  etransclem23  43661  etransclem36  43674  etransclem38  43676  carageniuncllem1  43922  0ome  43930  ovn02  43969  smflimlem4  44169  smflim  44172  smflim2  44199  smflimsup  44221  smfliminf  44224  fmtno0  44853  fmtno1  44854  fmtno2  44863  fmtno3  44864  fmtno4  44865  fmtno5lem4  44869  139prmALT  44909  31prm  44910  5tcu2e40  44928  3exp4mod41  44929  41prothprmlem2  44931  41prothprm  44932  nnsum3primesgbe  45105  nnsum4primesodd  45109  nnsum4primesoddALTV  45110  nnsum4primeseven  45113  nnsum4primesevenALTV  45114  bgoldbtbndlem1  45118  tgoldbachlt  45129  cznrnglem  45372  2t6m3t4e0  45545  zlmodzxzldeplem3  45704  ackval0  45887  ackval1  45888  ackval2  45889  ackval3  45890  ackval40  45900  ackval42  45903  ackval50  45905  disjdifb  46016  iscnrm3rlem1  46095  mndtchom  46230  sec0  46321