Theorem 3eqtr2i 2763

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 2760	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2757	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  indif  4260  dfrab3  4299  iunidOLD  5041  cocnvcnv2  6258  fmptap  7172  cnvoprab  8067  fpar  8123  fodomr  9150  fodomfir  9350  jech9.3  9836  dju1dif  10195  alephadd  10599  distrnq  10983  ltanq  10993  ltrnq  11001  1p2e3  12391  halfpm6th  12471  numma  12760  numaddc  12764  6p5lem  12786  8p2e10  12796  binom2i  14233  faclbnd4lem1  14314  cats2cat  14883  0.999...  15899  flodddiv4  16434  6gcd4e2  16557  dfphi2  16793  mod2xnegi  17091  karatsuba  17103  1259lem1  17150  setc2obas  18110  oppgtopn  19340  symgplusg  19368  cmnbascntr  19791  mgptopn  20113  ply1plusg  22173  ply1vsca  22174  ply1mulr  22175  restcld  23126  cmpsublem  23353  kgentopon  23492  dfii5  24847  itg1climres  25685  pigt3  26496  ang180lem1  26788  1cubrlem  26820  quart1lem  26834  efiatan  26891  log2cnv  26923  log2ublem3  26927  1sgm2ppw  27180  ppiub  27184  bposlem8  27271  bposlem9  27272  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  bday1s  27812  addsasslem2  27973  seqsval  28230  pw2bday  28354  ax5seglem7  28880  wlknwwlksnbij  29836  2pthd  29888  3pthd  30121  ipidsq  30657  ipdirilem  30776  norm3difi  31094  polid2i  31104  pjclem3  32144  cvmdi  32271  indifundif  32471  dpmul  32835  tocyccntz  33103  ccfldextdgrr  33659  eulerpartlemt  34332  eulerpart  34343  ballotlem1  34448  ballotlemfval0  34457  ballotth  34499  hgt750lem  34625  hgt750lem2  34626  subfaclim  35152  kur14lem6  35175  quad3  35634  iexpire  35694  volsupnfl  37631  dfxrn2  38336  xrninxp  38352  ipiiie0  42430  sn-0tie0  42432  areaquad  43191  wallispilem4  46040  dirkertrigeqlem3  46072  dirkercncflem1  46075  fourierswlem  46202  fouriersw  46203  smflimsuplem8  46799  ceil5half3  47300  3exp4mod41  47561  41prothprm  47564  tgoldbachlt  47761  zlmodzxz0  48230  linevalexample  48270  mndtcco  49190