Theorem 3eqtr4ri 2770

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  cbvreucsf  3940  dfin3  4266  dfsymdif3  4296  dfif6  4531  dfsn2ALT  4648  qdass  4757  tpidm12  4759  uniprOLD  4927  iinvdif  5083  unidif0  5358  csbcnv  5883  dfdm4  5895  dmun  5910  resres  5994  inres  5999  resdifcom  6000  resiun1  6001  imainrect  6180  cnvcnv  6191  coundi  6246  coundir  6247  funopg  6582  csbov  7455  elrnmpores  7549  offres  7973  1st2val  8006  2nd2val  8007  mpomptsx  8053  oeoalem  8599  omopthlem1  8661  snec  8777  tcsni  9741  infmap2  10216  ackbij2lem3  10239  itunisuc  10417  axmulass  11155  divmul13i  11980  dfnn3  12231  halfpm6th  12438  numsucc  12722  decbin2  12823  uzrdgxfr  13937  hashxplem  14398  prprrab  14439  ids1  14552  s3s4  14889  s2s5  14890  s5s2  14891  fsumadd  15691  fsum2d  15722  fprodmul  15909  bpoly3  16007  bezout  16490  ressbasOLD  17185  oppchomf  17671  dfinito3  17960  dftermo3  17961  smndex1iidm  18819  symgbas  19280  oppr1  20242  opsrtoslem1  21836  m2detleiblem2  22351  txswaphmeolem  23529  cnfldnm  24516  cnrbas  24890  cnnm  24909  volres  25278  voliunlem1  25300  uniioombllem4  25336  itg11  25441  dfrelog  26311  log2ublem3  26690  bposlem8  27031  noinfbnd2  27471  addsasslem1  27726  uhgrspan1  28828  ip2i  30349  bcseqi  30641  hilnormi  30684  cmcmlem  31112  fh3i  31144  fh4i  31145  pjadjii  31195  cnvoprabOLD  32213  resf1o  32223  dp3mul10  32332  dpmul4  32348  threehalves  32349  ressplusf  32395  cycpmconjs  32586  resvsca  32715  xpinpreima  33185  cnre2csqima  33190  esum2dlem  33389  eulerpartgbij  33670  ballotth  33835  plymulx  33858  hgt750lem2  33963  elrn3  35037  itg2addnclem2  36844  dfcoss3  37588  cossid  37654  dfssr2  37673  rabdif  41339  areaquad  42268  cnvrcl0  42679  stoweidlem13  45028  wallispi2  45088  fourierdlem96  45217  fourierdlem97  45218  fourierdlem98  45219  fourierdlem99  45220  fourierdlem113  45234  fourierswlem  45245  dfafv2  46139  dfnelbr2  46280  fmtnorec2  46510  fmtno5fac  46549  setrec2  47828