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  17661  dfinito3  17947  dftermo3  17948  smndex1iidm  18810  symgbas  19286  oppr1  20270  opsrtoslem1  21995  m2detleiblem2  22548  txswaphmeolem  23724  cnfldnm  24699  cnrbas  25075  cnnm  25093  volres  25462  voliunlem1  25484  uniioombllem4  25520  itg11  25625  dfrelog  26507  log2ublem3  26891  bposlem8  27235  noinfbnd2  27676  addsasslem1  27950  uhgrspan1  29283  ip2i  30807  bcseqi  31099  hilnormi  31142  cmcmlem  31570  fh3i  31602  fh4i  31603  pjadjii  31653  resf1o  32703  dp3mul10  32868  dpmul4  32884  threehalves  32885  ressplusf  32935  cycpmconjs  33128  resvsca  33297  cos9thpiminplylem5  33769  xpinpreima  33889  cnre2csqima  33894  esum2dlem  34075  eulerpartgbij  34356  ballotth  34522  plymulx  34532  hgt750lem2  34636  elrn3  35742  itg2addnclem2  37659  dfcoss3  38398  cossid  38464  dfssr2  38483  areaquad  43198  cnvrcl0  43607  stoweidlem13  46004  wallispi2  46064  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem113  46210  fourierswlem  46221  dfafv2  47126  dfnelbr2  47267  ceil5half3  47334  fmtnorec2  47537  fmtno5fac  47576  tposrescnv  48860  tposres3  48862  dfswapf2  49243  setrec2  49677