Theorem 3eqtr2i 2758

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  indif  4239  dfrab3  4278  iunidOLD  5020  cocnvcnv2  6219  fmptap  7126  cnvoprab  8018  fpar  8072  fodomr  9069  fodomfir  9255  jech9.3  9743  dju1dif  10102  alephadd  10506  distrnq  10890  ltanq  10900  ltrnq  10908  1p2e3  12300  halfpm6th  12380  numma  12669  numaddc  12673  6p5lem  12695  8p2e10  12705  binom2i  14153  faclbnd4lem1  14234  cats2cat  14804  0.999...  15823  flodddiv4  16361  6gcd4e2  16484  dfphi2  16720  mod2xnegi  17018  karatsuba  17030  1259lem1  17077  setc2obas  18036  oppgtopn  19267  symgplusg  19297  cmnbascntr  19719  mgptopn  20068  ply1plusg  22141  ply1vsca  22142  ply1mulr  22143  restcld  23092  cmpsublem  23319  kgentopon  23458  dfii5  24811  itg1climres  25648  pigt3  26460  ang180lem1  26752  1cubrlem  26784  quart1lem  26798  efiatan  26855  log2cnv  26887  log2ublem3  26891  1sgm2ppw  27144  ppiub  27148  bposlem8  27235  bposlem9  27236  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  bday1s  27780  addsasslem2  27951  seqsval  28222  ax5seglem7  28915  wlknwwlksnbij  29868  2pthd  29920  3pthd  30153  ipidsq  30689  ipdirilem  30808  norm3difi  31126  polid2i  31136  pjclem3  32176  cvmdi  32303  indifundif  32503  dpmul  32883  tocyccntz  33116  ccfldextdgrr  33660  cos9thpiminplylem5  33769  eulerpartlemt  34355  eulerpart  34366  ballotlem1  34471  ballotlemfval0  34480  ballotth  34522  hgt750lem  34635  hgt750lem2  34636  subfaclim  35168  kur14lem6  35191  quad3  35650  iexpire  35715  volsupnfl  37652  dfxrn2  38351  dmxrn  38353  xrninxp  38371  1p3e4  42240  ipiiie0  42419  sn-0tie0  42432  areaquad  43198  wallispilem4  46059  dirkertrigeqlem3  46091  dirkercncflem1  46094  fourierswlem  46221  fouriersw  46222  smflimsuplem8  46818  ceil5half3  47334  3exp4mod41  47610  41prothprm  47613  tgoldbachlt  47810  zlmodzxz0  48337  linevalexample  48377  mndtcco  49567