Theorem 3eqtr4ri 2775

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri

Step	Hyp	Ref	Expression
1		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
2		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtr4i 2767	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2767	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 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  cbvreucsf  3884  dfin3  4206  dfsymdif3  4236  dfif6  4468  dfsn2ALT  4585  qdass  4693  tpidm12  4695  uniprOLD  4863  iinvdif  5016  unidif0  5291  csbcnv  5805  dfdm4  5817  dmun  5832  resres  5916  inres  5921  resdifcom  5922  resiun1  5923  imainrect  6099  cnvcnv  6110  coundi  6165  coundir  6166  funopg  6497  csbov  7350  elrnmpores  7443  offres  7858  1st2val  7891  2nd2val  7892  mpomptsx  7936  oeoalem  8458  omopthlem1  8520  snec  8600  tcsni  9545  infmap2  10020  ackbij2lem3  10043  itunisuc  10221  axmulass  10959  divmul13i  11782  dfnn3  12033  halfpm6th  12240  numsucc  12523  decbin2  12624  uzrdgxfr  13733  hashxplem  14193  prprrab  14232  ids1  14347  s3s4  14691  s2s5  14692  s5s2  14693  fsumadd  15497  fsum2d  15528  fprodmul  15715  bpoly3  15813  bezout  16296  ressbasOLD  16993  oppchomf  17476  dfinito3  17765  dftermo3  17766  smndex1iidm  18585  symgbas  19023  oppr1  19921  opsrtoslem1  21307  m2detleiblem2  21822  txswaphmeolem  23000  cnfldnm  23987  cnrbas  24350  cnnm  24369  volres  24737  voliunlem1  24759  uniioombllem4  24795  itg11  24900  dfrelog  25766  log2ublem3  26143  bposlem8  26484  uhgrspan1  27715  ip2i  29235  bcseqi  29527  hilnormi  29570  cmcmlem  29998  fh3i  30030  fh4i  30031  pjadjii  30081  cnvoprabOLD  31100  resf1o  31110  dp3mul10  31217  dpmul4  31233  threehalves  31234  ressplusf  31280  cycpmconjs  31468  resvsca  31574  xpinpreima  31901  cnre2csqima  31906  esum2dlem  32105  eulerpartgbij  32384  ballotth  32549  plymulx  32572  hgt750lem2  32677  elrn3  33774  noinfbnd2  33979  itg2addnclem2  35873  dfcoss3  36582  cossid  36640  dfssr2  36659  rabdif  40226  areaquad  41085  cnvrcl0  41271  stoweidlem13  43603  wallispi2  43663  fourierdlem96  43792  fourierdlem97  43793  fourierdlem98  43794  fourierdlem99  43795  fourierdlem113  43809  fourierswlem  43820  dfafv2  44682  dfnelbr2  44823  fmtnorec2  45053  fmtno5fac  45092  setrec2  46459