Theorem 3eqtr4ri 2794

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  cbvreucsf  3891  dfin3  4223  dfsymdif3  4252  rabdif  4267  dfif6  4485  dfsn2ALT  4606  qdass  4714  tpidm12  4716  iinvdif  5040  unidif0OLD  5325  csbcnvOLD  5867  dfdm4  5879  dmun  5894  resres  5985  inres  5990  resdifcom  5991  resiun1  5992  imainrect  6174  cnvcnv  6185  coundi  6243  coundir  6244  funopg  6568  csbov  7459  elrnmpores  7552  offres  7981  1st2val  8015  2nd2val  8016  mpomptsx  8062  oeoalem  8585  omopthlem1  8648  snec  8779  tcsni  9721  infmap2  10220  ackbij2lem3  10243  itunisuc  10422  axmulass  11167  divmul13i  12001  dfnn3  12272  numsucc  12782  decbin2  12885  uzrdgxfr  14032  hashxplem  14499  prprrab  14539  ids1  14665  s3s4  15005  s2s5  15006  s5s2  15007  fsumadd  15827  fsum2d  15858  fprodmul  16048  bpoly3  16145  bezout  16634  oppchomf  17809  dfinito3  18095  dftermo3  18096  smndex1iidm  19011  symgbas  19500  oppr1  20492  opsrtoslem1  22272  m2detleiblem2  22851  txswaphmeolem  24031  cnfldnm  25005  cnrbas  25371  cnnm  25389  volres  25757  voliunlem1  25779  uniioombllem4  25815  itg11  25920  plymulidp  26513  dfrelog  26803  log2ublem3  27186  bposlem8  27528  noinfbnd2  27968  addsasslem1  28269  bdaypw2n0bndlem  28729  uhgrspan1  29764  ip2i  31310  bcseqi  31602  hilnormi  31645  cmcmlem  32073  fh3i  32105  fh4i  32106  pjadjii  32156  resf1o  33202  dp3mul10  33344  dpmul4  33360  threehalves  33361  ressplusf  33404  cycpmconjs  33597  resvsca  33773  cos9thpiminplylem5  34297  xpinpreima  34417  cnre2csqima  34422  esum2dlem  34603  eulerpartgbij  34884  ballotth  35050  hgt750lem2  35161  elrn3  36342  itg2addnclem2  38422  dfsucmap3  39212  dfsucmap4  39214  dfcoss3  39253  cossid  39319  dfssr2  39328  dfpetparts2  39721  dfpeters2  39723  areaquad  44058  cnvrcl0  44466  stoweidlem13  46842  wallispi2  46902  fourierdlem96  47031  fourierdlem97  47032  fourierdlem98  47033  fourierdlem99  47034  fourierdlem113  47048  fourierswlem  47059  goldpolyfactor  47746  goldratval  47755  dfafv2  48021  dfnelbr2  48162  ceil5half3  48235  fmtnorec2  48447  fmtno5fac  48486  tposrescnv  49806  tposres3  49808  dfswapf2  50188  setrec2  50622