Theorem 3eqtr4ri 2779

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  cbvreucsf  3968  dfin3  4296  dfsymdif3  4325  rabdif  4340  dfif6  4551  dfsn2ALT  4669  qdass  4778  tpidm12  4780  iinvdif  5103  unidif0  5378  csbcnv  5908  dfdm4  5920  dmun  5935  resres  6022  inres  6027  resdifcom  6028  resiun1  6029  imainrect  6212  cnvcnv  6223  coundi  6278  coundir  6279  funopg  6612  csbov  7493  elrnmpores  7588  offres  8024  1st2val  8058  2nd2val  8059  mpomptsx  8105  oeoalem  8652  omopthlem1  8715  snec  8838  tcsni  9812  infmap2  10286  ackbij2lem3  10309  itunisuc  10488  axmulass  11226  divmul13i  12055  dfnn3  12307  halfpm6th  12514  numsucc  12798  decbin2  12899  uzrdgxfr  14018  hashxplem  14482  prprrab  14522  ids1  14645  s3s4  14982  s2s5  14983  s5s2  14984  fsumadd  15788  fsum2d  15819  fprodmul  16008  bpoly3  16106  bezout  16590  ressbasOLD  17294  oppchomf  17780  dfinito3  18072  dftermo3  18073  smndex1iidm  18936  symgbas  19413  oppr1  20376  opsrtoslem1  22102  m2detleiblem2  22655  txswaphmeolem  23833  cnfldnm  24820  cnrbas  25194  cnnm  25213  volres  25582  voliunlem1  25604  uniioombllem4  25640  itg11  25745  dfrelog  26625  log2ublem3  27009  bposlem8  27353  noinfbnd2  27794  addsasslem1  28054  uhgrspan1  29338  ip2i  30860  bcseqi  31152  hilnormi  31195  cmcmlem  31623  fh3i  31655  fh4i  31656  pjadjii  31706  cnvoprabOLD  32734  resf1o  32744  dp3mul10  32862  dpmul4  32878  threehalves  32879  ressplusf  32930  cycpmconjs  33149  resvsca  33321  xpinpreima  33852  cnre2csqima  33857  esum2dlem  34056  eulerpartgbij  34337  ballotth  34502  plymulx  34525  hgt750lem2  34629  elrn3  35724  itg2addnclem2  37632  dfcoss3  38370  cossid  38436  dfssr2  38455  areaquad  43177  cnvrcl0  43587  stoweidlem13  45934  wallispi2  45994  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem113  46140  fourierswlem  46151  dfafv2  47047  dfnelbr2  47188  fmtnorec2  47417  fmtno5fac  47456  setrec2  48787