Theorem 3eqtr4ri 2797

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  cbvreucsf  3897  dfin3  4230  dfsymdif3  4259  rabdif  4274  dfif6  4490  dfsn2ALT  4611  qdass  4719  tpidm12  4721  iinvdif  5046  unidif0OLD  5331  csbcnvOLD  5873  dfdm4  5885  dmun  5900  resres  5991  inres  5996  resdifcom  5997  resiun1  5998  imainrect  6179  cnvcnv  6190  coundi  6248  coundir  6249  funopg  6570  csbov  7455  elrnmpores  7548  offres  7976  1st2val  8010  2nd2val  8011  mpomptsx  8057  oeoalem  8578  omopthlem1  8641  snec  8772  tcsni  9706  infmap2  10196  ackbij2lem3  10219  itunisuc  10398  axmulass  11137  divmul13i  11971  dfnn3  12242  numsucc  12751  decbin2  12854  uzrdgxfr  13999  hashxplem  14466  prprrab  14506  ids1  14631  s3s4  14966  s2s5  14967  s5s2  14968  fsumadd  15787  fsum2d  15818  fprodmul  16010  bpoly3  16107  bezout  16596  oppchomf  17771  dfinito3  18057  dftermo3  18058  smndex1iidm  18955  symgbas  19437  oppr1  20428  opsrtoslem1  22206  m2detleiblem2  22785  txswaphmeolem  23961  cnfldnm  24935  cnrbas  25301  cnnm  25319  volres  25687  voliunlem1  25709  uniioombllem4  25745  itg11  25850  plymulidp  26443  dfrelog  26730  log2ublem3  27113  bposlem8  27455  noinfbnd2  27895  addsasslem1  28196  bdaypw2n0bndlem  28656  uhgrspan1  29653  ip2i  31180  bcseqi  31472  hilnormi  31515  cmcmlem  31943  fh3i  31975  fh4i  31976  pjadjii  32026  resf1o  33075  dp3mul10  33217  dpmul4  33233  threehalves  33234  ressplusf  33283  cycpmconjs  33476  resvsca  33652  cos9thpiminplylem5  34176  xpinpreima  34296  cnre2csqima  34301  esum2dlem  34482  eulerpartgbij  34762  ballotth  34928  hgt750lem2  35039  elrn3  36254  itg2addnclem2  38323  dfsucmap3  39112  dfsucmap4  39114  dfcoss3  39153  cossid  39219  dfssr2  39228  dfpetparts2  39621  dfpeters2  39623  areaquad  43943  cnvrcl0  44351  stoweidlem13  46727  wallispi2  46787  fourierdlem96  46916  fourierdlem97  46917  fourierdlem98  46918  fourierdlem99  46919  fourierdlem113  46933  fourierswlem  46944  dfafv2  47869  dfnelbr2  48010  ceil5half3  48083  fmtnorec2  48295  fmtno5fac  48334  tposrescnv  49657  tposres3  49659  dfswapf2  50039  setrec2  50473