Theorem 3eqtr4ri 2778

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 2770	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2770	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 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  cbvreucsf  3883  dfin3  4205  dfsymdif3  4235  dfif6  4467  dfsn2ALT  4586  qdass  4694  tpidm12  4696  uniprOLD  4863  iinvdif  5013  unidif0  5285  csbcnv  5789  dfdm4  5801  dmun  5816  domepOLD  5830  resres  5901  inres  5906  resdifcom  5907  resiun1  5908  imainrect  6081  cnvcnv  6092  coundi  6148  coundir  6149  funopg  6464  csbov  7311  elrnmpores  7402  offres  7812  1st2val  7845  2nd2val  7846  mpomptsx  7890  oeoalem  8403  omopthlem1  8463  snec  8543  tcsni  9484  infmap2  9958  ackbij2lem3  9981  itunisuc  10159  axmulass  10897  divmul13i  11719  dfnn3  11970  halfpm6th  12177  numsucc  12459  decbin2  12560  uzrdgxfr  13668  hashxplem  14129  prprrab  14168  ids1  14283  s3s4  14627  s2s5  14628  s5s2  14629  fsumadd  15433  fsum2d  15464  fprodmul  15651  bpoly3  15749  bezout  16232  ressbasOLD  16929  oppchomf  17412  dfinito3  17701  dftermo3  17702  smndex1iidm  18521  symgbas  18959  oppr1  19857  opsrtoslem1  21243  m2detleiblem2  21758  txswaphmeolem  22936  cnfldnm  23923  cnrbas  24286  cnnm  24305  volres  24673  voliunlem1  24695  uniioombllem4  24731  itg11  24836  dfrelog  25702  log2ublem3  26079  bposlem8  26420  uhgrspan1  27651  ip2i  29169  bcseqi  29461  hilnormi  29504  cmcmlem  29932  fh3i  29964  fh4i  29965  pjadjii  30015  cnvoprabOLD  31034  resf1o  31044  dp3mul10  31151  dpmul4  31167  threehalves  31168  ressplusf  31214  cycpmconjs  31402  resvsca  31508  xpinpreima  31835  cnre2csqima  31840  esum2dlem  32039  eulerpartgbij  32318  ballotth  32483  plymulx  32506  hgt750lem2  32611  elrn3  33708  noinfbnd2  33913  itg2addnclem2  35808  dfcoss3  36519  cossid  36577  dfssr2  36596  rabdif  40164  areaquad  41027  cnvrcl0  41186  stoweidlem13  43508  wallispi2  43568  fourierdlem96  43697  fourierdlem97  43698  fourierdlem98  43699  fourierdlem99  43700  fourierdlem113  43714  fourierswlem  43725  dfafv2  44575  dfnelbr2  44716  fmtnorec2  44947  fmtno5fac  44986  setrec2  46353