Theorem 3eqtr2i 2789

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  indif  4224  dfrab3  4263  cocnvcnv2  6263  fmptap  7179  cnvoprab  8075  fpar  8133  fodomr  9154  fodomfir  9326  jech9.3OLD  9830  dju1dif  10258  alephadd  10669  distrnq  11053  ltanq  11063  ltrnq  11071  1p2e3  12492  halfpm6th  12575  numma  12870  numaddc  12874  6p5lem  12896  8p2e10  12906  binom2i  14363  faclbnd4lem1  14444  cats2cat  15021  0.999...  16059  flodddiv4  16594  6gcd4e2  16720  dfphi2  16960  mod2xnegi  17258  karatsuba  17270  1259lem1  17318  setc2obas  18278  oppgtopn  19576  symgplusg  19606  cmnbascntr  20028  mgptopn  20377  ply1plusg  22550  ply1vsca  22551  ply1mulr  22552  restcld  23499  cmpsublem  23726  kgentopon  23866  dfii5  25215  itg1climres  26044  pigt3  26855  ang180lem1  27146  1cubrlem  27178  quart1lem  27192  efiatan  27249  log2cnv  27281  log2ublem3  27285  1sgm2ppw  27536  ppiub  27540  bposlem8  27627  bposlem9  27628  2lgsoddprmlem3c  27748  2lgsoddprmlem3d  27749  bday1  28209  addsasslem2  28399  seqsval  28683  ax5seglem7  29522  wlknwwlksnbij  30486  2pthd  30538  3pthd  30784  ipidsq  31321  ipdirilem  31440  norm3difi  31758  polid2i  31768  pjclem3  32808  cvmdi  32935  indifundif  33171  dpmul  33529  tocyccntz  33755  ccfldextdgrr  34354  cos9thpiminplylem5  34468  eulerpartlemt  35053  eulerpart  35064  ballotlem1  35169  ballotlemfval0  35178  ballotth  35220  hgt750lem  35330  hgt750lem2  35331  subfaclim  36043  kur14lem6  36066  quad3  36525  iexpire  36596  volsupnfl  38692  dfxrn2  39426  dmxrn  39428  dmxrnuncnvepres  39433  xrninxp  39456  1p3e4  43419  1p4e5  43420  1p5e6  43421  1p6e7  43422  1p7e8  43423  1p8e9  43424  4p5e9  43433  ipiiie0  43598  sn-0tie0  43624  areaquad  44327  wallispilem4  47186  dirkertrigeqlem3  47218  dirkercncflem1  47221  fourierswlem  47348  fouriersw  47349  smflimsuplem8  47945  goldpolyfactor  48035  ceil5half3  48524  3exp4mod41  48809  41prothprm  48812  tgoldbachlt  49022  zlmodzxz0  49576  linevalexample  49615  mndtcco  50831