Theorem 3eqtr2i 2772

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 2769	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2766	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  indif  4200  dfrab3  4240  iunid  4986  cocnvcnv2  6151  fmptap  7024  cnvoprab  7873  fpar  7927  fodomr  8864  jech9.3  9503  dju1dif  9859  alephadd  10264  distrnq  10648  ltanq  10658  ltrnq  10666  1p2e3  12046  halfpm6th  12124  numma  12410  numaddc  12414  6p5lem  12436  8p2e10  12446  binom2i  13856  faclbnd4lem1  13935  cats2cat  14503  0.999...  15521  flodddiv4  16050  6gcd4e2  16174  dfphi2  16403  mod2xnegi  16700  karatsuba  16713  1259lem1  16760  setc2obas  17725  oppgtopn  18875  symgplusg  18905  mgptopn  19647  ply1plusg  21306  ply1vsca  21307  ply1mulr  21308  restcld  22231  cmpsublem  22458  kgentopon  22597  dfii5  23954  itg1climres  24784  pigt3  25579  ang180lem1  25864  1cubrlem  25896  quart1lem  25910  efiatan  25967  log2cnv  25999  log2ublem3  26003  1sgm2ppw  26253  ppiub  26257  bposlem8  26344  bposlem9  26345  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  ax5seglem7  27206  wlknwwlksnbij  28154  2pthd  28206  3pthd  28439  ipidsq  28973  ipdirilem  29092  norm3difi  29410  polid2i  29420  pjclem3  30460  cvmdi  30587  indifundif  30774  dpmul  31089  tocyccntz  31313  ccfldextdgrr  31644  eulerpartlemt  32238  eulerpart  32249  ballotlem1  32353  ballotlemfval0  32362  ballotth  32404  hgt750lem  32531  hgt750lem2  32532  subfaclim  33050  kur14lem6  33073  quad3  33528  iexpire  33607  bday1s  33952  volsupnfl  35749  dfxrn2  36433  xrninxp  36445  ipiiie0  40340  sn-0tie0  40342  areaquad  40963  wallispilem4  43499  dirkertrigeqlem3  43531  dirkercncflem1  43534  fourierswlem  43661  fouriersw  43662  smflimsuplem8  44247  3exp4mod41  44956  41prothprm  44959  tgoldbachlt  45156  zlmodzxz0  45580  linevalexample  45624  mndtcco  46258