Theorem 3eqtr4ri 2770

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 2762	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2762	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  cbvreucsf  3940  dfin3  4266  dfsymdif3  4296  dfif6  4531  dfsn2ALT  4648  qdass  4757  tpidm12  4759  uniprOLD  4927  iinvdif  5083  unidif0  5358  csbcnv  5883  dfdm4  5895  dmun  5910  resres  5994  inres  5999  resdifcom  6000  resiun1  6001  imainrect  6180  cnvcnv  6191  coundi  6246  coundir  6247  funopg  6582  csbov  7455  elrnmpores  7549  offres  7974  1st2val  8007  2nd2val  8008  mpomptsx  8054  oeoalem  8602  omopthlem1  8664  snec  8780  tcsni  9744  infmap2  10219  ackbij2lem3  10242  itunisuc  10420  axmulass  11158  divmul13i  11982  dfnn3  12233  halfpm6th  12440  numsucc  12724  decbin2  12825  uzrdgxfr  13939  hashxplem  14400  prprrab  14441  ids1  14554  s3s4  14891  s2s5  14892  s5s2  14893  fsumadd  15693  fsum2d  15724  fprodmul  15911  bpoly3  16009  bezout  16492  ressbasOLD  17187  oppchomf  17673  dfinito3  17965  dftermo3  17966  smndex1iidm  18824  symgbas  19286  oppr1  20248  opsrtoslem1  21927  m2detleiblem2  22450  txswaphmeolem  23628  cnfldnm  24615  cnrbas  24989  cnnm  25008  volres  25377  voliunlem1  25399  uniioombllem4  25435  itg11  25540  dfrelog  26414  log2ublem3  26794  bposlem8  27137  noinfbnd2  27577  addsasslem1  27833  uhgrspan1  28993  ip2i  30514  bcseqi  30806  hilnormi  30849  cmcmlem  31277  fh3i  31309  fh4i  31310  pjadjii  31360  cnvoprabOLD  32378  resf1o  32388  dp3mul10  32497  dpmul4  32513  threehalves  32514  ressplusf  32560  cycpmconjs  32751  resvsca  32880  xpinpreima  33350  cnre2csqima  33355  esum2dlem  33554  eulerpartgbij  33835  ballotth  34000  plymulx  34023  hgt750lem2  34128  elrn3  35202  itg2addnclem2  37004  dfcoss3  37748  cossid  37814  dfssr2  37833  rabdif  41499  areaquad  42428  cnvrcl0  42839  stoweidlem13  45188  wallispi2  45248  fourierdlem96  45377  fourierdlem97  45378  fourierdlem98  45379  fourierdlem99  45380  fourierdlem113  45394  fourierswlem  45405  dfafv2  46299  dfnelbr2  46440  fmtnorec2  46670  fmtno5fac  46709  setrec2  47902