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  3903  dfin3  4236  dfsymdif3  4265  rabdif  4280  dfif6  4487  dfsn2ALT  4607  qdass  4713  tpidm12  4715  iinvdif  5039  unidif0  5310  csbcnv  5837  dfdm4  5849  dmun  5864  resres  5952  inres  5957  resdifcom  5958  resiun1  5959  imainrect  6142  cnvcnv  6153  coundi  6208  coundir  6209  funopg  6534  csbov  7414  elrnmpores  7507  offres  7941  1st2val  7975  2nd2val  7976  mpomptsx  8022  oeoalem  8537  omopthlem1  8600  snec  8728  tcsni  9672  infmap2  10146  ackbij2lem3  10169  itunisuc  10348  axmulass  11086  divmul13i  11919  dfnn3  12176  numsucc  12665  decbin2  12766  uzrdgxfr  13908  hashxplem  14374  prprrab  14414  ids1  14538  s3s4  14875  s2s5  14876  s5s2  14877  fsumadd  15682  fsum2d  15713  fprodmul  15902  bpoly3  16000  bezout  16489  oppchomf  17657  dfinito3  17943  dftermo3  17944  smndex1iidm  18804  symgbas  19278  oppr1  20235  opsrtoslem1  21938  m2detleiblem2  22491  txswaphmeolem  23667  cnfldnm  24642  cnrbas  25018  cnnm  25036  volres  25405  voliunlem1  25427  uniioombllem4  25463  itg11  25568  dfrelog  26450  log2ublem3  26834  bposlem8  27178  noinfbnd2  27619  addsasslem1  27886  uhgrspan1  29206  ip2i  30730  bcseqi  31022  hilnormi  31065  cmcmlem  31493  fh3i  31525  fh4i  31526  pjadjii  31576  resf1o  32626  dp3mul10  32791  dpmul4  32807  threehalves  32808  ressplusf  32858  cycpmconjs  33086  resvsca  33277  cos9thpiminplylem5  33749  xpinpreima  33869  cnre2csqima  33874  esum2dlem  34055  eulerpartgbij  34336  ballotth  34502  plymulx  34512  hgt750lem2  34616  elrn3  35722  itg2addnclem2  37639  dfcoss3  38378  cossid  38444  dfssr2  38463  areaquad  43178  cnvrcl0  43587  stoweidlem13  45984  wallispi2  46044  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem113  46190  fourierswlem  46201  dfafv2  47106  dfnelbr2  47247  ceil5half3  47314  fmtnorec2  47517  fmtno5fac  47556  tposrescnv  48840  tposres3  48842  dfswapf2  49223  setrec2  49657