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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  indif  4226  dfrab3  4265  cocnvcnv2  6255  fmptap  7168  cnvoprab  8057  fpar  8113  fodomr  9126  fodomfir  9297  jech9.3  9796  dju1dif  10175  alephadd  10586  distrnq  10970  ltanq  10980  ltrnq  10988  1p2e3  12407  halfpm6th  12490  numma  12785  numaddc  12789  6p5lem  12811  8p2e10  12821  binom2i  14276  faclbnd4lem1  14357  cats2cat  14933  0.999...  15970  flodddiv4  16505  6gcd4e2  16628  dfphi2  16865  mod2xnegi  17163  karatsuba  17175  1259lem1  17223  setc2obas  18183  oppgtopn  19480  symgplusg  19510  cmnbascntr  19932  mgptopn  20281  ply1plusg  22448  ply1vsca  22449  ply1mulr  22450  restcld  23397  cmpsublem  23624  kgentopon  23764  dfii5  25113  itg1climres  25942  pigt3  26755  ang180lem1  27046  1cubrlem  27078  quart1lem  27092  efiatan  27149  log2cnv  27181  log2ublem3  27185  1sgm2ppw  27436  ppiub  27440  bposlem8  27527  bposlem9  27528  2lgsoddprmlem3c  27648  2lgsoddprmlem3d  27649  bday1  28079  addsasslem2  28269  seqsval  28553  ax5seglem7  29392  wlknwwlksnbij  30356  2pthd  30408  3pthd  30654  ipidsq  31191  ipdirilem  31310  norm3difi  31628  polid2i  31638  pjclem3  32678  cvmdi  32805  indifundif  32999  dpmul  33358  tocyccntz  33584  ccfldextdgrr  34182  cos9thpiminplylem5  34296  eulerpartlemt  34882  eulerpart  34893  ballotlem1  34998  ballotlemfval0  35007  ballotth  35049  hgt750lem  35159  hgt750lem2  35160  subfaclim  35767  kur14lem6  35790  quad3  36249  iexpire  36314  volsupnfl  38414  dfxrn2  39133  dmxrn  39135  dmxrnuncnvepres  39140  xrninxp  39163  1p3e4  43126  1p4e5  43127  1p5e6  43128  1p6e7  43129  1p7e8  43130  1p8e9  43131  4p5e9  43140  ipiiie0  43313  sn-0tie0  43339  areaquad  44057  wallispilem4  46896  dirkertrigeqlem3  46928  dirkercncflem1  46931  fourierswlem  47058  fouriersw  47059  smflimsuplem8  47655  goldpolyfactor  47745  ceil5half3  48234  3exp4mod41  48519  41prothprm  48522  tgoldbachlt  48732  zlmodzxz0  49286  linevalexample  49325  mndtcco  50511