Theorem 3eqtr4ri 2795

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

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

This theorem is used by:  cbvreucsf  3891  dfin3  4223  dfsymdif3  4252  rabdif  4267  dfif6  4485  dfsn2ALT  4606  qdass  4714  tpidm12  4716  iinvdif  5040  unidif0OLD  5322  csbcnvOLD  5865  dfdm4  5877  dmun  5892  resres  5983  inres  5988  resdifcom  5989  resiun1  5990  imainrect  6173  cnvcnv  6184  coundi  6248  coundir  6249  funopg  6574  csbov  7465  elrnmpores  7558  offres  7995  1st2val  8029  2nd2val  8030  mpomptsx  8075  oeoalem  8605  omopthlem1  8668  snec  8799  tcsni  9742  dfhf2  9906  setrec2  9977  infmap2  10295  ackbij2lem3  10318  itunisuc  10497  axmulass  11242  divmul13i  12078  dfnn3  12349  numsucc  12859  decbin2  12962  uzrdgxfr  14110  hashxplem  14578  prprrab  14618  ids1  14744  s3s4  15084  s2s5  15085  s5s2  15086  fsumadd  15906  fsum2d  15937  fprodmul  16127  bpoly3  16224  bezout  16716  oppchomf  17894  dfinito3  18180  dftermo3  18181  smndex1iidm  19097  symgbas  19586  oppr1  20580  opsrtoslem1  22364  m2detleiblem2  22943  txswaphmeolem  24123  cnfldnm  25097  cnrbas  25463  cnnm  25481  volres  25849  voliunlem1  25871  uniioombllem4  25907  itg11  26012  plymulidp  26603  dfrelog  26893  log2ublem3  27276  bposlem8  27618  noinfbnd2  28088  addsasslem1  28389  bdaypw2n0bndlem  28849  uhgrspan1  29884  ip2i  31430  bcseqi  31722  hilnormi  31765  cmcmlem  32193  fh3i  32225  fh4i  32226  pjadjii  32276  resf1o  33322  dp3mul10  33464  dpmul4  33480  threehalves  33481  ressplusf  33524  cycpmconjs  33717  resvsca  33893  cos9thpiminplylem5  34418  xpinpreima  34538  cnre2csqima  34543  esum2dlem  34724  eulerpartgbij  35004  ballotth  35170  hgt750lem2  35281  elrn3  36527  itg2addnclem2  38590  dfsucmap3  39395  dfsucmap4  39397  dfcoss3  39436  cossid  39502  dfssr2  39511  dfpetparts2  39904  dfpeters2  39906  areaquad  44217  cnvrcl0  44624  stoweidlem13  47022  wallispi2  47082  fourierdlem96  47211  fourierdlem97  47212  fourierdlem98  47213  fourierdlem99  47214  fourierdlem113  47228  fourierswlem  47239  goldpolyfactor  47926  goldratval  47935  dfafv2  48201  dfnelbr2  48342  ceil5half3  48415  fmtnorec2  48627  fmtno5fac  48666  tposrescnv  49986  tposres3  49988  dfswapf2  50368