Theorem 3eqtr2i 2767

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 2764	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2761	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  indif  4269  dfrab3  4309  iunidOLD  5064  cocnvcnv2  6255  fmptap  7165  cnvoprab  8043  fpar  8099  fodomr  9125  jech9.3  9806  dju1dif  10164  alephadd  10569  distrnq  10953  ltanq  10963  ltrnq  10971  1p2e3  12352  halfpm6th  12430  numma  12718  numaddc  12722  6p5lem  12744  8p2e10  12754  binom2i  14173  faclbnd4lem1  14250  cats2cat  14810  0.999...  15824  flodddiv4  16353  6gcd4e2  16477  dfphi2  16704  mod2xnegi  17001  karatsuba  17014  1259lem1  17061  setc2obas  18041  oppgtopn  19215  symgplusg  19245  cmnbascntr  19668  mgptopn  19994  ply1plusg  21739  ply1vsca  21740  ply1mulr  21741  restcld  22668  cmpsublem  22895  kgentopon  23034  dfii5  24393  itg1climres  25224  pigt3  26019  ang180lem1  26304  1cubrlem  26336  quart1lem  26350  efiatan  26407  log2cnv  26439  log2ublem3  26443  1sgm2ppw  26693  ppiub  26697  bposlem8  26784  bposlem9  26785  2lgsoddprmlem3c  26905  2lgsoddprmlem3d  26906  bday1s  27322  addsasslem2  27477  ax5seglem7  28183  wlknwwlksnbij  29132  2pthd  29184  3pthd  29417  ipidsq  29951  ipdirilem  30070  norm3difi  30388  polid2i  30398  pjclem3  31438  cvmdi  31565  indifundif  31750  dpmul  32067  tocyccntz  32291  ccfldextdgrr  32735  eulerpartlemt  33359  eulerpart  33370  ballotlem1  33474  ballotlemfval0  33483  ballotth  33525  hgt750lem  33652  hgt750lem2  33653  subfaclim  34168  kur14lem6  34191  quad3  34644  iexpire  34694  volsupnfl  36522  dfxrn2  37235  xrninxp  37251  ipiiie0  41307  sn-0tie0  41309  areaquad  41951  wallispilem4  44771  dirkertrigeqlem3  44803  dirkercncflem1  44806  fourierswlem  44933  fouriersw  44934  smflimsuplem8  45530  3exp4mod41  46271  41prothprm  46274  tgoldbachlt  46471  zlmodzxz0  46986  linevalexample  47030  mndtcco  47665