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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  cbvreucsf  3881  dfin3  4217  dfsymdif3  4246  rabdif  4261  dfif6  4469  dfsn2ALT  4589  qdass  4697  tpidm12  4699  iinvdif  5022  unidif0OLD  5302  csbcnv  5838  dfdm4  5850  dmun  5865  resres  5957  inres  5962  resdifcom  5963  resiun1  5964  imainrect  6145  cnvcnv  6156  coundi  6211  coundir  6212  funopg  6532  csbov  7412  elrnmpores  7505  offres  7936  1st2val  7970  2nd2val  7971  mpomptsx  8017  oeoalem  8532  omopthlem1  8595  snec  8725  tcsni  9662  infmap2  10139  ackbij2lem3  10162  itunisuc  10341  axmulass  11080  divmul13i  11916  dfnn3  12188  numsucc  12684  decbin2  12785  uzrdgxfr  13929  hashxplem  14395  prprrab  14435  ids1  14560  s3s4  14895  s2s5  14896  s5s2  14897  fsumadd  15702  fsum2d  15733  fprodmul  15925  bpoly3  16023  bezout  16512  oppchomf  17686  dfinito3  17972  dftermo3  17973  smndex1iidm  18869  symgbas  19347  oppr1  20330  opsrtoslem1  22033  m2detleiblem2  22593  txswaphmeolem  23769  cnfldnm  24743  cnrbas  25109  cnnm  25127  volres  25495  voliunlem1  25517  uniioombllem4  25553  itg11  25658  dfrelog  26529  log2ublem3  26912  bposlem8  27254  noinfbnd2  27695  addsasslem1  27995  bdaypw2n0bndlem  28455  uhgrspan1  29372  ip2i  30899  bcseqi  31191  hilnormi  31234  cmcmlem  31662  fh3i  31694  fh4i  31695  pjadjii  31745  resf1o  32803  dp3mul10  32957  dpmul4  32973  threehalves  32974  ressplusf  33023  cycpmconjs  33217  resvsca  33392  cos9thpiminplylem5  33930  xpinpreima  34050  cnre2csqima  34055  esum2dlem  34236  eulerpartgbij  34516  ballotth  34682  plymulx  34692  hgt750lem2  34796  elrn3  35944  itg2addnclem2  37993  dfsucmap3  38784  dfsucmap4  38786  dfcoss3  38825  cossid  38891  dfssr2  38900  dfpetparts2  39293  dfpeters2  39295  areaquad  43644  cnvrcl0  44052  stoweidlem13  46441  wallispi2  46501  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem113  46647  fourierswlem  46658  dfafv2  47580  dfnelbr2  47721  ceil5half3  47794  fmtnorec2  48006  fmtno5fac  48045  tposrescnv  49354  tposres3  49356  dfswapf2  49736  setrec2  50170