Theorem 3eqtr4ri 2643

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  cbvreucsf  3533  dfin3  3825  dfsymdif3  3852  dfif6  4039  qdass  4232  tpidm12  4234  opid  4359  unipr  4385  iinvdif  4528  unidif0  4764  csbcnv  5228  dfdm4  5238  dmun  5253  resres  5329  inres  5334  resdifcom  5335  resiun1  5336  resiun1OLD  5337  imainrect  5494  coundi  5553  coundir  5554  funopg  5836  csbov  6586  elrnmpt2res  6672  offres  7054  1st2val  7085  2nd2val  7086  mpt2mptsx  7122  oeoalem  7563  omopthlem1  7622  snec  7697  tcsni  8502  infmap2  8923  ackbij2lem3  8946  itunisuc  9124  axmulass  9857  divmul13i  10665  dfnn3  10911  halfpm6th  11130  numsucc  11425  decbin2  11559  uzrdgxfr  12628  hashxplem  13080  prprrab  13112  ids1  13230  s3s4  13528  s2s5  13529  s5s2  13530  fsumadd  14317  fsum2d  14344  fprodmul  14529  bpoly3  14628  bezout  15098  ressbas  15757  oppchomf  16203  oppr1  18457  opsrtoslem1  19305  m2detleiblem2  20253  cnfldnm  22392  cnnm  22768  volres  23103  voliunlem1  23125  uniioombllem4  23160  itg11  23264  plyid  23769  coeidp  23823  dgrid  23824  dfrelog  24116  log2ublem3  24475  bposlem8  24816  ip2i  27067  bcseqi  27361  hilnormi  27404  cmcmlem  27834  fh3i  27866  fh4i  27867  pjadjii  27917  cnvoprab  28886  resf1o  28893  ressplusf  28981  resvsca  29161  xpinpreima  29280  cnre2csqima  29285  esum2dlem  29481  eulerpartgbij  29761  ballotth  29926  plymulx  29951  elrn3  30906  domep  30942  itg2addnclem2  32632  areaquad  36821  cnvrcl0  36951  stoweidlem13  38906  wallispi2  38966  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem113  39112  fourierswlem  39123  fmtnorec2  39993  fmtno5fac  40032  uhgrspan1  40527  setrec2  42241