Theorem 3eqtr4ri 2765

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  cbvreucsf  3889  dfin3  4224  dfsymdif3  4253  rabdif  4268  dfif6  4475  dfsn2ALT  4595  qdass  4703  tpidm12  4705  iinvdif  5026  unidif0  5296  csbcnv  5822  dfdm4  5834  dmun  5849  resres  5940  inres  5945  resdifcom  5946  resiun1  5947  imainrect  6128  cnvcnv  6139  coundi  6194  coundir  6195  funopg  6515  csbov  7391  elrnmpores  7484  offres  7915  1st2val  7949  2nd2val  7950  mpomptsx  7996  oeoalem  8511  omopthlem1  8574  snec  8702  tcsni  9631  infmap2  10108  ackbij2lem3  10131  itunisuc  10310  axmulass  11048  divmul13i  11882  dfnn3  12139  numsucc  12628  decbin2  12729  uzrdgxfr  13874  hashxplem  14340  prprrab  14380  ids1  14505  s3s4  14840  s2s5  14841  s5s2  14842  fsumadd  15647  fsum2d  15678  fprodmul  15867  bpoly3  15965  bezout  16454  oppchomf  17626  dfinito3  17912  dftermo3  17913  smndex1iidm  18809  symgbas  19284  oppr1  20268  opsrtoslem1  21990  m2detleiblem2  22543  txswaphmeolem  23719  cnfldnm  24693  cnrbas  25069  cnnm  25087  volres  25456  voliunlem1  25478  uniioombllem4  25514  itg11  25619  dfrelog  26501  log2ublem3  26885  bposlem8  27229  noinfbnd2  27670  addsasslem1  27946  uhgrspan1  29281  ip2i  30808  bcseqi  31100  hilnormi  31143  cmcmlem  31571  fh3i  31603  fh4i  31604  pjadjii  31654  resf1o  32713  dp3mul10  32878  dpmul4  32894  threehalves  32895  ressplusf  32944  cycpmconjs  33125  resvsca  33297  cos9thpiminplylem5  33799  xpinpreima  33919  cnre2csqima  33924  esum2dlem  34105  eulerpartgbij  34385  ballotth  34551  plymulx  34561  hgt750lem2  34665  elrn3  35806  itg2addnclem2  37722  dfsucmap3  38486  dfsucmap4  38488  dfcoss3  38526  cossid  38592  dfssr2  38601  dfblockliftfix2  38746  areaquad  43319  cnvrcl0  43728  stoweidlem13  46121  wallispi2  46181  fourierdlem96  46310  fourierdlem97  46311  fourierdlem98  46312  fourierdlem99  46313  fourierdlem113  46327  fourierswlem  46338  dfafv2  47242  dfnelbr2  47383  ceil5half3  47450  fmtnorec2  47653  fmtno5fac  47692  tposrescnv  48989  tposres3  48991  dfswapf2  49372  setrec2  49806