Theorem 3eqtr4ri 2799

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  cbvreucsf  3898  dfin3  4230  dfsymdif3  4259  rabdif  4274  dfif6  4492  dfsn2ALT  4613  qdass  4721  tpidm12  4723  iinvdif  5048  unidif0OLD  5333  csbcnvOLD  5875  dfdm4  5887  dmun  5902  resres  5993  inres  5998  resdifcom  5999  resiun1  6000  imainrect  6181  cnvcnv  6192  coundi  6250  coundir  6251  funopg  6574  csbov  7464  elrnmpores  7557  offres  7986  1st2val  8020  2nd2val  8021  mpomptsx  8067  oeoalem  8588  omopthlem1  8651  snec  8782  tcsni  9717  infmap2  10216  ackbij2lem3  10239  itunisuc  10418  axmulass  11157  divmul13i  11991  dfnn3  12262  numsucc  12772  decbin2  12875  uzrdgxfr  14021  hashxplem  14488  prprrab  14528  ids1  14654  s3s4  14994  s2s5  14995  s5s2  14996  fsumadd  15814  fsum2d  15845  fprodmul  16037  bpoly3  16134  bezout  16623  oppchomf  17798  dfinito3  18084  dftermo3  18085  smndex1iidm  18997  symgbas  19486  oppr1  20478  opsrtoslem1  22256  m2detleiblem2  22835  txswaphmeolem  24012  cnfldnm  24986  cnrbas  25352  cnnm  25370  volres  25738  voliunlem1  25760  uniioombllem4  25796  itg11  25901  plymulidp  26494  dfrelog  26781  log2ublem3  27164  bposlem8  27506  noinfbnd2  27946  addsasslem1  28247  bdaypw2n0bndlem  28707  uhgrspan1  29711  ip2i  31251  bcseqi  31543  hilnormi  31586  cmcmlem  32014  fh3i  32046  fh4i  32047  pjadjii  32097  resf1o  33145  dp3mul10  33287  dpmul4  33303  threehalves  33304  ressplusf  33347  cycpmconjs  33540  resvsca  33716  cos9thpiminplylem5  34240  xpinpreima  34360  cnre2csqima  34365  esum2dlem  34546  eulerpartgbij  34827  ballotth  34993  hgt750lem2  35104  elrn3  36291  itg2addnclem2  38380  dfsucmap3  39170  dfsucmap4  39172  dfcoss3  39211  cossid  39277  dfssr2  39286  dfpetparts2  39679  dfpeters2  39681  areaquad  44001  cnvrcl0  44409  stoweidlem13  46785  wallispi2  46845  fourierdlem96  46974  fourierdlem97  46975  fourierdlem98  46976  fourierdlem99  46977  fourierdlem113  46991  fourierswlem  47002  dfafv2  47927  dfnelbr2  48068  ceil5half3  48141  fmtnorec2  48353  fmtno5fac  48392  tposrescnv  49714  tposres3  49716  dfswapf2  50096  setrec2  50530