Theorem 3eqtr2i 2850

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  indif  4245  dfrab3  4277  iunid  4976  cocnvcnv2  6105  fmptap  6926  cnvoprab  7752  fpar  7805  fodomr  8662  jech9.3  9237  dju1dif  9592  alephadd  9993  distrnq  10377  ltanq  10387  ltrnq  10395  1p2e3  11774  halfpm6th  11852  numma  12136  numaddc  12140  6p5lem  12162  8p2e10  12172  binom2i  13568  faclbnd4lem1  13647  cats2cat  14218  0.999...  15231  flodddiv4  15758  6gcd4e2  15880  dfphi2  16105  mod2xnegi  16401  karatsuba  16414  1259lem1  16458  oppgtopn  18475  symgplusg  18505  mgptopn  19242  ply1plusg  20387  ply1vsca  20388  ply1mulr  20389  restcld  21774  cmpsublem  22001  kgentopon  22140  dfii5  23487  itg1climres  24309  pigt3  25097  ang180lem1  25381  1cubrlem  25413  quart1lem  25427  efiatan  25484  log2cnv  25516  log2ublem3  25520  1sgm2ppw  25770  ppiub  25774  bposlem8  25861  bposlem9  25862  2lgsoddprmlem3c  25982  2lgsoddprmlem3d  25983  ax5seglem7  26715  wlknwwlksnbij  27660  2pthd  27713  3pthd  27947  ipidsq  28481  ipdirilem  28600  norm3difi  28918  polid2i  28928  pjclem3  29968  cvmdi  30095  indifundif  30279  dpmul  30584  tocyccntz  30781  ccfldextdgrr  31052  eulerpartlemt  31624  eulerpart  31635  ballotlem1  31739  ballotlemfval0  31748  ballotth  31790  hgt750lem  31917  hgt750lem2  31918  subfaclim  32430  kur14lem6  32453  quad3  32908  iexpire  32962  volsupnfl  34931  dfxrn2  35622  xrninxp  35634  areaquad  39816  wallispilem4  42347  dirkertrigeqlem3  42379  dirkercncflem1  42382  fourierswlem  42509  fouriersw  42510  smflimsuplem8  43095  3exp4mod41  43775  41prothprm  43778  tgoldbachlt  43975  zlmodzxz0  44398  linevalexample  44444