Theorem 3eqtr4ri 2796

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  cbvreucsf  3896  dfin3  4229  dfsymdif3  4258  rabdif  4273  dfif6  4483  dfsn2ALT  4604  qdass  4712  tpidm12  4714  iinvdif  5037  unidif0OLD  5317  csbcnvOLD  5859  dfdm4  5871  dmun  5886  resres  5978  inres  5983  resdifcom  5984  resiun1  5985  imainrect  6167  cnvcnv  6178  coundi  6234  coundir  6235  funopg  6555  csbov  7441  elrnmpores  7534  offres  7964  1st2val  7998  2nd2val  7999  mpomptsx  8045  oeoalem  8566  omopthlem1  8629  snec  8760  tcsni  9696  infmap2  10173  ackbij2lem3  10196  itunisuc  10376  axmulass  11115  divmul13i  11952  dfnn3  12224  numsucc  12733  decbin2  12836  uzrdgxfr  13980  hashxplem  14446  prprrab  14486  ids1  14611  s3s4  14946  s2s5  14947  s5s2  14948  fsumadd  15767  fsum2d  15798  fprodmul  15990  bpoly3  16088  bezout  16577  oppchomf  17752  dfinito3  18038  dftermo3  18039  smndex1iidm  18935  symgbas  19412  oppr1  20399  opsrtoslem1  22108  m2detleiblem2  22688  txswaphmeolem  23864  cnfldnm  24838  cnrbas  25204  cnnm  25222  volres  25590  voliunlem1  25612  uniioombllem4  25648  itg11  25753  plymulidp  26346  dfrelog  26630  log2ublem3  27013  bposlem8  27355  noinfbnd2  27795  addsasslem1  28096  bdaypw2n0bndlem  28556  uhgrspan1  29504  ip2i  31031  bcseqi  31323  hilnormi  31366  cmcmlem  31794  fh3i  31826  fh4i  31827  pjadjii  31877  resf1o  32932  dp3mul10  33075  dpmul4  33091  threehalves  33092  ressplusf  33141  cycpmconjs  33336  resvsca  33518  cos9thpiminplylem5  34083  xpinpreima  34203  cnre2csqima  34208  esum2dlem  34389  eulerpartgbij  34669  ballotth  34835  hgt750lem2  34946  elrn3  36112  itg2addnclem2  38171  dfsucmap3  38962  dfsucmap4  38964  dfcoss3  39003  cossid  39069  dfssr2  39078  dfpetparts2  39471  dfpeters2  39473  areaquad  43793  cnvrcl0  44201  stoweidlem13  46587  wallispi2  46647  fourierdlem96  46776  fourierdlem97  46777  fourierdlem98  46778  fourierdlem99  46779  fourierdlem113  46793  fourierswlem  46804  dfafv2  47726  dfnelbr2  47867  ceil5half3  47940  fmtnorec2  48152  fmtno5fac  48191  tposrescnv  49500  tposres3  49502  dfswapf2  49882  setrec2  50316