Theorem 3eqtr4ri 2763

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 2755	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2755	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  cbvreucsf  3906  dfin3  4240  dfsymdif3  4269  rabdif  4284  dfif6  4491  dfsn2ALT  4611  qdass  4717  tpidm12  4719  iinvdif  5044  unidif0  5315  csbcnv  5847  dfdm4  5859  dmun  5874  resres  5963  inres  5968  resdifcom  5969  resiun1  5970  imainrect  6154  cnvcnv  6165  coundi  6220  coundir  6221  funopg  6550  csbov  7432  elrnmpores  7527  offres  7962  1st2val  7996  2nd2val  7997  mpomptsx  8043  oeoalem  8560  omopthlem1  8623  snec  8751  tcsni  9696  infmap2  10170  ackbij2lem3  10193  itunisuc  10372  axmulass  11110  divmul13i  11943  dfnn3  12200  numsucc  12689  decbin2  12790  uzrdgxfr  13932  hashxplem  14398  prprrab  14438  ids1  14562  s3s4  14899  s2s5  14900  s5s2  14901  fsumadd  15706  fsum2d  15737  fprodmul  15926  bpoly3  16024  bezout  16513  oppchomf  17681  dfinito3  17967  dftermo3  17968  smndex1iidm  18828  symgbas  19302  oppr1  20259  opsrtoslem1  21962  m2detleiblem2  22515  txswaphmeolem  23691  cnfldnm  24666  cnrbas  25042  cnnm  25060  volres  25429  voliunlem1  25451  uniioombllem4  25487  itg11  25592  dfrelog  26474  log2ublem3  26858  bposlem8  27202  noinfbnd2  27643  addsasslem1  27910  uhgrspan1  29230  ip2i  30757  bcseqi  31049  hilnormi  31092  cmcmlem  31520  fh3i  31552  fh4i  31553  pjadjii  31603  resf1o  32653  dp3mul10  32818  dpmul4  32834  threehalves  32835  ressplusf  32885  cycpmconjs  33113  resvsca  33304  cos9thpiminplylem5  33776  xpinpreima  33896  cnre2csqima  33901  esum2dlem  34082  eulerpartgbij  34363  ballotth  34529  plymulx  34539  hgt750lem2  34643  elrn3  35749  itg2addnclem2  37666  dfcoss3  38405  cossid  38471  dfssr2  38490  areaquad  43205  cnvrcl0  43614  stoweidlem13  46011  wallispi2  46071  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem113  46217  fourierswlem  46228  dfafv2  47133  dfnelbr2  47274  ceil5half3  47341  fmtnorec2  47544  fmtno5fac  47583  tposrescnv  48867  tposres3  48869  dfswapf2  49250  setrec2  49684