Theorem 3eqtr4ri 2774

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 2766	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2766	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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  cbvreucsf  3955  dfin3  4283  dfsymdif3  4312  rabdif  4327  dfif6  4534  dfsn2ALT  4652  qdass  4758  tpidm12  4760  iinvdif  5085  unidif0  5366  csbcnv  5897  dfdm4  5909  dmun  5924  resres  6013  inres  6018  resdifcom  6019  resiun1  6020  imainrect  6203  cnvcnv  6214  coundi  6269  coundir  6270  funopg  6602  csbov  7476  elrnmpores  7571  offres  8007  1st2val  8041  2nd2val  8042  mpomptsx  8088  oeoalem  8633  omopthlem1  8696  snec  8819  tcsni  9781  infmap2  10255  ackbij2lem3  10278  itunisuc  10457  axmulass  11195  divmul13i  12026  dfnn3  12278  halfpm6th  12485  numsucc  12771  decbin2  12872  uzrdgxfr  14005  hashxplem  14469  prprrab  14509  ids1  14632  s3s4  14969  s2s5  14970  s5s2  14971  fsumadd  15773  fsum2d  15804  fprodmul  15993  bpoly3  16091  bezout  16577  ressbasOLD  17281  oppchomf  17767  dfinito3  18059  dftermo3  18060  smndex1iidm  18927  symgbas  19404  oppr1  20367  opsrtoslem1  22097  m2detleiblem2  22650  txswaphmeolem  23828  cnfldnm  24815  cnrbas  25189  cnnm  25208  volres  25577  voliunlem1  25599  uniioombllem4  25635  itg11  25740  dfrelog  26622  log2ublem3  27006  bposlem8  27350  noinfbnd2  27791  addsasslem1  28051  uhgrspan1  29335  ip2i  30857  bcseqi  31149  hilnormi  31192  cmcmlem  31620  fh3i  31652  fh4i  31653  pjadjii  31703  cnvoprabOLD  32738  resf1o  32748  dp3mul10  32865  dpmul4  32881  threehalves  32882  ressplusf  32933  cycpmconjs  33159  resvsca  33336  xpinpreima  33867  cnre2csqima  33872  esum2dlem  34073  eulerpartgbij  34354  ballotth  34519  plymulx  34542  hgt750lem2  34646  elrn3  35742  itg2addnclem2  37659  dfcoss3  38396  cossid  38462  dfssr2  38481  areaquad  43205  cnvrcl0  43615  stoweidlem13  45969  wallispi2  46029  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem113  46175  fourierswlem  46186  dfafv2  47082  dfnelbr2  47223  ceil5half3  47280  fmtnorec2  47468  fmtno5fac  47507  setrec2  48926