Theorem 3eqtr2i 2766

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 2763	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2760	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  indif  4221  dfrab3  4260  cocnvcnv2  6217  fmptap  7118  cnvoprab  8006  fpar  8059  fodomr  9059  fodomfir  9231  jech9.3  9729  dju1dif  10086  alephadd  10491  distrnq  10875  ltanq  10885  ltrnq  10893  1p2e3  12310  halfpm6th  12390  numma  12679  numaddc  12683  6p5lem  12705  8p2e10  12715  binom2i  14165  faclbnd4lem1  14246  cats2cat  14815  0.999...  15837  flodddiv4  16375  6gcd4e2  16498  dfphi2  16735  mod2xnegi  17033  karatsuba  17045  1259lem1  17092  setc2obas  18052  oppgtopn  19319  symgplusg  19349  cmnbascntr  19771  mgptopn  20120  ply1plusg  22197  ply1vsca  22198  ply1mulr  22199  restcld  23147  cmpsublem  23374  kgentopon  23513  dfii5  24862  itg1climres  25691  pigt3  26495  ang180lem1  26786  1cubrlem  26818  quart1lem  26832  efiatan  26889  log2cnv  26921  log2ublem3  26925  1sgm2ppw  27177  ppiub  27181  bposlem8  27268  bposlem9  27269  2lgsoddprmlem3c  27389  2lgsoddprmlem3d  27390  bday1  27820  addsasslem2  28010  seqsval  28294  ax5seglem7  29018  wlknwwlksnbij  29971  2pthd  30023  3pthd  30259  ipidsq  30796  ipdirilem  30915  norm3difi  31233  polid2i  31243  pjclem3  32283  cvmdi  32410  indifundif  32609  dpmul  32987  tocyccntz  33220  ccfldextdgrr  33832  cos9thpiminplylem5  33946  eulerpartlemt  34531  eulerpart  34542  ballotlem1  34647  ballotlemfval0  34656  ballotth  34698  hgt750lem  34811  hgt750lem2  34812  subfaclim  35386  kur14lem6  35409  quad3  35868  iexpire  35933  volsupnfl  38000  dfxrn2  38720  dmxrn  38722  dmxrnuncnvepres  38727  xrninxp  38750  1p3e4  42711  ipiiie0  42884  sn-0tie0  42910  areaquad  43662  wallispilem4  46514  dirkertrigeqlem3  46546  dirkercncflem1  46549  fourierswlem  46676  fouriersw  46677  smflimsuplem8  47273  ceil5half3  47806  3exp4mod41  48091  41prothprm  48094  tgoldbachlt  48304  zlmodzxz0  48844  linevalexample  48883  mndtcco  50072