Theorem 3eqtr4ri 2655

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

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  cbvreucsf  3567  dfin3  3866  dfsymdif3  3893  dfif6  4089  qdass  4288  tpidm12  4290  opid  4421  unipr  4449  iinvdif  4592  unidif0  4838  csbcnv  5306  dfdm4  5316  dmun  5331  resres  5409  inres  5414  resdifcom  5415  resiun1  5416  resiun1OLD  5417  imainrect  5575  cnvcnv  5586  coundi  5636  coundir  5637  funopg  5922  csbov  6688  elrnmpt2res  6774  offres  7163  1st2val  7194  2nd2val  7195  mpt2mptsx  7233  oeoalem  7676  omopthlem1  7735  snec  7810  tcsni  8619  infmap2  9040  ackbij2lem3  9063  itunisuc  9241  axmulass  9978  divmul13i  10786  dfnn3  11034  halfpm6th  11253  numsucc  11549  decbin2  11683  uzrdgxfr  12766  hashxplem  13220  prprrab  13255  ids1  13377  s3s4  13678  s2s5  13679  s5s2  13680  fsumadd  14470  fsum2d  14502  fprodmul  14690  bpoly3  14789  bezout  15260  ressbas  15930  oppchomf  16380  oppr1  18634  opsrtoslem1  19484  m2detleiblem2  20434  cnfldnm  22582  cnnm  22960  volres  23296  voliunlem1  23318  uniioombllem4  23354  itg11  23458  plyid  23965  coeidp  24019  dgrid  24020  dfrelog  24312  log2ublem3  24675  bposlem8  25016  uhgrspan1  26195  ip2i  27683  bcseqi  27977  hilnormi  28020  cmcmlem  28450  fh3i  28482  fh4i  28483  pjadjii  28533  cnvoprab  29498  resf1o  29505  dp3mul10  29606  dpmul4  29622  threehalves  29623  ressplusf  29650  resvsca  29830  xpinpreima  29952  cnre2csqima  29957  esum2dlem  30154  eulerpartgbij  30434  ballotth  30599  plymulx  30625  hgt750lem2  30730  elrn3  31652  domep  31698  itg2addnclem2  33462  areaquad  37802  cnvrcl0  37932  stoweidlem13  40230  wallispi2  40290  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem113  40436  fourierswlem  40447  dfnelbr2  41290  fmtnorec2  41455  fmtno5fac  41494  setrec2  42442