Theorem 3eqtr4ri 2832

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  cbvreucsf  3872  dfin3  4193  dfsymdif3  4221  dfif6  4428  dfsn2ALT  4545  qdass  4649  tpidm12  4651  unipr  4817  iinvdif  4965  unidif0  5225  csbcnv  5718  dfdm4  5728  dmun  5743  domepOLD  5758  resres  5831  inres  5836  resdifcom  5837  resiun1  5838  imainrect  6005  cnvcnv  6016  coundi  6067  coundir  6068  funopg  6358  csbov  7178  elrnmpores  7267  offres  7666  1st2val  7699  2nd2val  7700  mpomptsx  7744  oeoalem  8205  omopthlem1  8265  snec  8343  tcsni  9169  infmap2  9629  ackbij2lem3  9652  itunisuc  9830  axmulass  10568  divmul13i  11390  dfnn3  11639  halfpm6th  11846  numsucc  12126  decbin2  12227  uzrdgxfr  13330  hashxplem  13790  prprrab  13827  ids1  13942  s3s4  14286  s2s5  14287  s5s2  14288  fsumadd  15088  fsum2d  15118  fprodmul  15306  bpoly3  15404  bezout  15881  ressbas  16546  oppchomf  16982  smndex1iidm  18058  symgbas  18491  oppr1  19380  opsrtoslem1  20723  m2detleiblem2  21233  txswaphmeolem  22409  cnfldnm  23384  cnrbas  23747  cnnm  23765  volres  24132  voliunlem1  24154  uniioombllem4  24190  itg11  24295  dfrelog  25157  log2ublem3  25534  bposlem8  25875  uhgrspan1  27093  ip2i  28611  bcseqi  28903  hilnormi  28946  cmcmlem  29374  fh3i  29406  fh4i  29407  pjadjii  29457  cnvoprabOLD  30482  resf1o  30492  dp3mul10  30600  dpmul4  30616  threehalves  30617  ressplusf  30663  cycpmconjs  30848  resvsca  30954  xpinpreima  31259  cnre2csqima  31264  esum2dlem  31461  eulerpartgbij  31740  ballotth  31905  plymulx  31928  hgt750lem2  32033  elrn3  33111  itg2addnclem2  35109  dfcoss3  35822  cossid  35880  dfssr2  35899  rabdif  39399  areaquad  40166  cnvrcl0  40325  stoweidlem13  42655  wallispi2  42715  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem113  42861  fourierswlem  42872  dfafv2  43688  dfnelbr2  43829  fmtnorec2  44060  fmtno5fac  44099  setrec2  45225