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  4270  dfrab3  4310  iunidOLD  5065  cocnvcnv2  6258  fmptap  7168  cnvoprab  8046  fpar  8102  fodomr  9128  jech9.3  9809  dju1dif  10167  alephadd  10572  distrnq  10956  ltanq  10966  ltrnq  10974  1p2e3  12355  halfpm6th  12433  numma  12721  numaddc  12725  6p5lem  12747  8p2e10  12757  binom2i  14176  faclbnd4lem1  14253  cats2cat  14813  0.999...  15827  flodddiv4  16356  6gcd4e2  16480  dfphi2  16707  mod2xnegi  17004  karatsuba  17017  1259lem1  17064  setc2obas  18044  oppgtopn  19220  symgplusg  19250  cmnbascntr  19673  mgptopn  19999  ply1plusg  21747  ply1vsca  21748  ply1mulr  21749  restcld  22676  cmpsublem  22903  kgentopon  23042  dfii5  24401  itg1climres  25232  pigt3  26027  ang180lem1  26314  1cubrlem  26346  quart1lem  26360  efiatan  26417  log2cnv  26449  log2ublem3  26453  1sgm2ppw  26703  ppiub  26707  bposlem8  26794  bposlem9  26795  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  bday1s  27333  addsasslem2  27490  ax5seglem7  28224  wlknwwlksnbij  29173  2pthd  29225  3pthd  29458  ipidsq  29994  ipdirilem  30113  norm3difi  30431  polid2i  30441  pjclem3  31481  cvmdi  31608  indifundif  31793  dpmul  32110  tocyccntz  32334  ccfldextdgrr  32777  eulerpartlemt  33401  eulerpart  33412  ballotlem1  33516  ballotlemfval0  33525  ballotth  33567  hgt750lem  33694  hgt750lem2  33695  subfaclim  34210  kur14lem6  34233  quad3  34686  iexpire  34736  volsupnfl  36581  dfxrn2  37294  xrninxp  37310  ipiiie0  41358  sn-0tie0  41360  areaquad  42013  wallispilem4  44832  dirkertrigeqlem3  44864  dirkercncflem1  44867  fourierswlem  44994  fouriersw  44995  smflimsuplem8  45591  3exp4mod41  46332  41prothprm  46335  tgoldbachlt  46532  zlmodzxz0  47080  linevalexample  47124  mndtcco  47759