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 1541

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  cbvreucsf  3893  dfin3  4229  dfsymdif3  4258  rabdif  4273  dfif6  4482  dfsn2ALT  4602  qdass  4710  tpidm12  4712  iinvdif  5035  unidif0  5305  csbcnv  5832  dfdm4  5844  dmun  5859  resres  5951  inres  5956  resdifcom  5957  resiun1  5958  imainrect  6139  cnvcnv  6150  coundi  6205  coundir  6206  funopg  6526  csbov  7403  elrnmpores  7496  offres  7927  1st2val  7961  2nd2val  7962  mpomptsx  8008  oeoalem  8524  omopthlem1  8587  snec  8715  tcsni  9650  infmap2  10127  ackbij2lem3  10150  itunisuc  10329  axmulass  11068  divmul13i  11902  dfnn3  12159  numsucc  12647  decbin2  12748  uzrdgxfr  13890  hashxplem  14356  prprrab  14396  ids1  14521  s3s4  14856  s2s5  14857  s5s2  14858  fsumadd  15663  fsum2d  15694  fprodmul  15883  bpoly3  15981  bezout  16470  oppchomf  17643  dfinito3  17929  dftermo3  17930  smndex1iidm  18826  symgbas  19301  oppr1  20286  opsrtoslem1  22010  m2detleiblem2  22572  txswaphmeolem  23748  cnfldnm  24722  cnrbas  25098  cnnm  25116  volres  25485  voliunlem1  25507  uniioombllem4  25543  itg11  25648  dfrelog  26530  log2ublem3  26914  bposlem8  27258  noinfbnd2  27699  addsasslem1  27999  bdaypw2n0bndlem  28459  uhgrspan1  29376  ip2i  30903  bcseqi  31195  hilnormi  31238  cmcmlem  31666  fh3i  31698  fh4i  31699  pjadjii  31749  resf1o  32809  dp3mul10  32979  dpmul4  32995  threehalves  32996  ressplusf  33045  cycpmconjs  33238  resvsca  33413  cos9thpiminplylem5  33943  xpinpreima  34063  cnre2csqima  34068  esum2dlem  34249  eulerpartgbij  34529  ballotth  34695  plymulx  34705  hgt750lem2  34809  elrn3  35956  itg2addnclem2  37873  dfsucmap3  38637  dfsucmap4  38639  dfcoss3  38677  cossid  38743  dfssr2  38752  dfblockliftfix2  38897  areaquad  43458  cnvrcl0  43866  stoweidlem13  46257  wallispi2  46317  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem113  46463  fourierswlem  46474  dfafv2  47378  dfnelbr2  47519  ceil5half3  47586  fmtnorec2  47789  fmtno5fac  47828  tposrescnv  49124  tposres3  49126  dfswapf2  49506  setrec2  49940