Theorem 3eqtr4ri 2860

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

Syntax hints:   = wceq 1658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2818

This theorem is referenced by:  cbvreucsf  3791  dfin3  4096  dfsymdif3  4122  dfif6  4309  dfsn2ALT  4417  qdass  4506  tpidm12  4508  unipr  4671  iinvdif  4812  unidif0  5060  csbcnv  5538  dfdm4  5548  dmun  5563  resres  5646  inres  5651  resdifcom  5652  resiun1  5653  imainrect  5816  cnvcnv  5827  coundi  5877  coundir  5878  funopg  6157  csbov  6947  elrnmpt2res  7034  offres  7423  1st2val  7456  2nd2val  7457  mpt2mptsx  7496  oeoalem  7943  omopthlem1  8002  snec  8075  tcsni  8896  infmap2  9355  ackbij2lem3  9378  itunisuc  9556  axmulass  10294  divmul13i  11112  dfnn3  11366  halfpm6th  11579  numsucc  11862  decbin2  11964  uzrdgxfr  13061  hashxplem  13509  prprrab  13544  ids1  13657  s3s4  14054  s2s5  14055  s5s2  14056  fsumadd  14847  fsum2d  14877  fprodmul  15063  bpoly3  15161  bezout  15633  ressbas  16293  oppchomf  16732  oppr1  18988  opsrtoslem1  19844  m2detleiblem2  20802  cnfldnm  22952  cnnm  23329  volres  23694  voliunlem1  23716  uniioombllem4  23752  itg11  23857  plyid  24364  coeidp  24418  dgrid  24419  dfrelog  24711  log2ublem3  25088  bposlem8  25429  uhgrspan1  26600  ip2i  28238  bcseqi  28532  hilnormi  28575  cmcmlem  29005  fh3i  29037  fh4i  29038  pjadjii  29088  cnvoprabOLD  30046  resf1o  30053  dp3mul10  30151  dpmul4  30167  threehalves  30168  ressplusf  30195  resvsca  30375  xpinpreima  30497  cnre2csqima  30502  esum2dlem  30699  eulerpartgbij  30979  ballotth  31145  plymulx  31172  hgt750lem2  31279  elrn3  32194  domep  32236  itg2addnclem2  34005  dfcoss3  34720  cossid  34778  dfssr2  34797  areaquad  38644  cnvrcl0  38773  stoweidlem13  41024  wallispi2  41084  fourierdlem96  41213  fourierdlem97  41214  fourierdlem98  41215  fourierdlem99  41216  fourierdlem113  41230  fourierswlem  41241  dfafv2  42034  dfnelbr2  42175  fmtnorec2  42285  fmtno5fac  42324  setrec2  43337