Theorem 3eqtr4ri 2776

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 2768	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2768	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  cbvreucsf  3943  dfin3  4277  dfsymdif3  4306  rabdif  4321  dfif6  4528  dfsn2ALT  4647  qdass  4753  tpidm12  4755  iinvdif  5080  unidif0  5360  csbcnv  5894  dfdm4  5906  dmun  5921  resres  6010  inres  6015  resdifcom  6016  resiun1  6017  imainrect  6201  cnvcnv  6212  coundi  6267  coundir  6268  funopg  6600  csbov  7476  elrnmpores  7571  offres  8008  1st2val  8042  2nd2val  8043  mpomptsx  8089  oeoalem  8634  omopthlem1  8697  snec  8820  tcsni  9783  infmap2  10257  ackbij2lem3  10280  itunisuc  10459  axmulass  11197  divmul13i  12028  dfnn3  12280  halfpm6th  12487  numsucc  12773  decbin2  12874  uzrdgxfr  14008  hashxplem  14472  prprrab  14512  ids1  14635  s3s4  14972  s2s5  14973  s5s2  14974  fsumadd  15776  fsum2d  15807  fprodmul  15996  bpoly3  16094  bezout  16580  ressbasOLD  17281  oppchomf  17763  dfinito3  18050  dftermo3  18051  smndex1iidm  18914  symgbas  19389  oppr1  20350  opsrtoslem1  22079  m2detleiblem2  22634  txswaphmeolem  23812  cnfldnm  24799  cnrbas  25175  cnnm  25194  volres  25563  voliunlem1  25585  uniioombllem4  25621  itg11  25726  dfrelog  26607  log2ublem3  26991  bposlem8  27335  noinfbnd2  27776  addsasslem1  28036  uhgrspan1  29320  ip2i  30847  bcseqi  31139  hilnormi  31182  cmcmlem  31610  fh3i  31642  fh4i  31643  pjadjii  31693  resf1o  32741  dp3mul10  32880  dpmul4  32896  threehalves  32897  ressplusf  32948  cycpmconjs  33176  resvsca  33356  xpinpreima  33905  cnre2csqima  33910  esum2dlem  34093  eulerpartgbij  34374  ballotth  34540  plymulx  34563  hgt750lem2  34667  elrn3  35762  itg2addnclem2  37679  dfcoss3  38415  cossid  38481  dfssr2  38500  areaquad  43228  cnvrcl0  43638  stoweidlem13  46028  wallispi2  46088  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem113  46234  fourierswlem  46245  dfafv2  47144  dfnelbr2  47285  ceil5half3  47342  fmtnorec2  47530  fmtno5fac  47569  tposrescnv  48779  tposres3  48781  dfswapf2  48967  setrec2  49214