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 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  indif  4203  dfrab3  4243  iunid  4990  cocnvcnv2  6162  fmptap  7042  cnvoprab  7900  fpar  7956  fodomr  8915  jech9.3  9572  dju1dif  9928  alephadd  10333  distrnq  10717  ltanq  10727  ltrnq  10735  1p2e3  12116  halfpm6th  12194  numma  12481  numaddc  12485  6p5lem  12507  8p2e10  12517  binom2i  13928  faclbnd4lem1  14007  cats2cat  14575  0.999...  15593  flodddiv4  16122  6gcd4e2  16246  dfphi2  16475  mod2xnegi  16772  karatsuba  16785  1259lem1  16832  setc2obas  17809  oppgtopn  18960  symgplusg  18990  mgptopn  19732  ply1plusg  21396  ply1vsca  21397  ply1mulr  21398  restcld  22323  cmpsublem  22550  kgentopon  22689  dfii5  24048  itg1climres  24879  pigt3  25674  ang180lem1  25959  1cubrlem  25991  quart1lem  26005  efiatan  26062  log2cnv  26094  log2ublem3  26098  1sgm2ppw  26348  ppiub  26352  bposlem8  26439  bposlem9  26440  2lgsoddprmlem3c  26560  2lgsoddprmlem3d  26561  ax5seglem7  27303  wlknwwlksnbij  28253  2pthd  28305  3pthd  28538  ipidsq  29072  ipdirilem  29191  norm3difi  29509  polid2i  29519  pjclem3  30559  cvmdi  30686  indifundif  30873  dpmul  31187  tocyccntz  31411  ccfldextdgrr  31742  eulerpartlemt  32338  eulerpart  32349  ballotlem1  32453  ballotlemfval0  32462  ballotth  32504  hgt750lem  32631  hgt750lem2  32632  subfaclim  33150  kur14lem6  33173  quad3  33628  iexpire  33701  bday1s  34025  volsupnfl  35822  dfxrn2  36506  xrninxp  36518  ipiiie0  40419  sn-0tie0  40421  areaquad  41047  wallispilem4  43609  dirkertrigeqlem3  43641  dirkercncflem1  43644  fourierswlem  43771  fouriersw  43772  smflimsuplem8  44360  3exp4mod41  45068  41prothprm  45071  tgoldbachlt  45268  zlmodzxz0  45692  linevalexample  45736  mndtcco  46372