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  6567  csbov  7458  elrnmpores  7551  offres  7980  1st2val  8014  2nd2val  8015  mpomptsx  8061  oeoalem  8584  omopthlem1  8647  snec  8778  tcsni  9720  infmap2  10219  ackbij2lem3  10242  itunisuc  10421  axmulass  11166  divmul13i  12000  dfnn3  12271  numsucc  12781  decbin2  12884  uzrdgxfr  14031  hashxplem  14498  prprrab  14538  ids1  14664  s3s4  15004  s2s5  15005  s5s2  15006  fsumadd  15826  fsum2d  15857  fprodmul  16047  bpoly3  16144  bezout  16633  oppchomf  17808  dfinito3  18094  dftermo3  18095  smndex1iidm  19010  symgbas  19499  oppr1  20491  opsrtoslem1  22271  m2detleiblem2  22850  txswaphmeolem  24030  cnfldnm  25004  cnrbas  25370  cnnm  25388  volres  25756  voliunlem1  25778  uniioombllem4  25814  itg11  25919  plymulidp  26512  dfrelog  26802  log2ublem3  27185  bposlem8  27527  noinfbnd2  27967  addsasslem1  28268  bdaypw2n0bndlem  28728  uhgrspan1  29763  ip2i  31309  bcseqi  31601  hilnormi  31644  cmcmlem  32072  fh3i  32104  fh4i  32105  pjadjii  32155  resf1o  33201  dp3mul10  33343  dpmul4  33359  threehalves  33360  ressplusf  33403  cycpmconjs  33596  resvsca  33772  cos9thpiminplylem5  34296  xpinpreima  34416  cnre2csqima  34421  esum2dlem  34602  eulerpartgbij  34883  ballotth  35049  hgt750lem2  35160  elrn3  36341  itg2addnclem2  38421  dfsucmap3  39211  dfsucmap4  39213  dfcoss3  39252  cossid  39318  dfssr2  39327  dfpetparts2  39720  dfpeters2  39722  areaquad  44057  cnvrcl0  44465  stoweidlem13  46841  wallispi2  46901  fourierdlem96  47030  fourierdlem97  47031  fourierdlem98  47032  fourierdlem99  47033  fourierdlem113  47047  fourierswlem  47058  goldpolyfactor  47745  goldratval  47754  dfafv2  48020  dfnelbr2  48161  ceil5half3  48234  fmtnorec2  48446  fmtno5fac  48485  tposrescnv  49805  tposres3  49807  dfswapf2  50187  setrec2  50621