Theorem 3eqtr4ri 2684

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

Syntax hints:   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  cbvreucsf  3600  dfin3  3899  dfsymdif3  3926  dfif6  4122  qdass  4320  tpidm12  4322  unipr  4481  iinvdif  4624  unidif0  4868  csbcnv  5338  dfdm4  5348  dmun  5363  resres  5444  inres  5449  resdifcom  5450  resiun1  5451  resiun1OLD  5452  imainrect  5610  cnvcnv  5621  coundi  5674  coundir  5675  funopg  5960  csbov  6728  elrnmpt2res  6816  offres  7205  1st2val  7238  2nd2val  7239  mpt2mptsx  7278  oeoalem  7721  omopthlem1  7780  snec  7853  tcsni  8657  infmap2  9078  ackbij2lem3  9101  itunisuc  9279  axmulass  10016  divmul13i  10824  dfnn3  11072  halfpm6th  11291  numsucc  11587  decbin2  11721  uzrdgxfr  12806  hashxplem  13258  prprrab  13293  ids1  13413  s3s4  13724  s2s5  13725  s5s2  13726  fsumadd  14514  fsum2d  14546  fprodmul  14734  bpoly3  14833  bezout  15307  ressbas  15977  oppchomf  16427  oppr1  18680  opsrtoslem1  19532  m2detleiblem2  20482  cnfldnm  22629  cnnm  23006  volres  23342  voliunlem1  23364  uniioombllem4  23400  itg11  23503  plyid  24010  coeidp  24064  dgrid  24065  dfrelog  24357  log2ublem3  24720  bposlem8  25061  uhgrspan1  26240  ip2i  27811  bcseqi  28105  hilnormi  28148  cmcmlem  28578  fh3i  28610  fh4i  28611  pjadjii  28661  cnvoprabOLD  29626  resf1o  29633  dp3mul10  29734  dpmul4  29750  threehalves  29751  ressplusf  29778  resvsca  29958  xpinpreima  30080  cnre2csqima  30085  esum2dlem  30282  eulerpartgbij  30562  ballotth  30727  plymulx  30753  hgt750lem2  30858  elrn3  31778  domep  31822  itg2addnclem2  33592  dfcoss3  34312  cossid  34370  dfssr2  34389  areaquad  38119  cnvrcl0  38249  stoweidlem13  40548  wallispi2  40608  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem113  40754  fourierswlem  40765  dfnelbr2  41614  fmtnorec2  41780  fmtno5fac  41819  setrec2  42767