Theorem 3eqtr2i 2774

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2i	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2771	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2768	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  indif  4209  dfrab3  4249  iunid  4995  cocnvcnv2  6161  fmptap  7039  cnvoprab  7893  fpar  7947  fodomr  8897  jech9.3  9573  dju1dif  9929  alephadd  10334  distrnq  10718  ltanq  10728  ltrnq  10736  1p2e3  12116  halfpm6th  12194  numma  12480  numaddc  12484  6p5lem  12506  8p2e10  12516  binom2i  13926  faclbnd4lem1  14005  cats2cat  14573  0.999...  15591  flodddiv4  16120  6gcd4e2  16244  dfphi2  16473  mod2xnegi  16770  karatsuba  16783  1259lem1  16830  setc2obas  17807  oppgtopn  18958  symgplusg  18988  mgptopn  19730  ply1plusg  21394  ply1vsca  21395  ply1mulr  21396  restcld  22321  cmpsublem  22548  kgentopon  22687  dfii5  24046  itg1climres  24877  pigt3  25672  ang180lem1  25957  1cubrlem  25989  quart1lem  26003  efiatan  26060  log2cnv  26092  log2ublem3  26096  1sgm2ppw  26346  ppiub  26350  bposlem8  26437  bposlem9  26438  2lgsoddprmlem3c  26558  2lgsoddprmlem3d  26559  ax5seglem7  27301  wlknwwlksnbij  28249  2pthd  28301  3pthd  28534  ipidsq  29068  ipdirilem  29187  norm3difi  29505  polid2i  29515  pjclem3  30555  cvmdi  30682  indifundif  30869  dpmul  31183  tocyccntz  31407  ccfldextdgrr  31738  eulerpartlemt  32334  eulerpart  32345  ballotlem1  32449  ballotlemfval0  32458  ballotth  32500  hgt750lem  32627  hgt750lem2  32628  subfaclim  33146  kur14lem6  33169  quad3  33624  iexpire  33697  bday1s  34021  volsupnfl  35818  dfxrn2  36502  xrninxp  36514  ipiiie0  40416  sn-0tie0  40418  areaquad  41044  wallispilem4  43580  dirkertrigeqlem3  43612  dirkercncflem1  43615  fourierswlem  43742  fouriersw  43743  smflimsuplem8  44328  3exp4mod41  45037  41prothprm  45040  tgoldbachlt  45237  zlmodzxz0  45661  linevalexample  45705  mndtcco  46341