Theorem 3eqtr2i 2794

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 2791	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2788	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 2156  ax-ext 2737

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

This theorem is used by:  indif  4233  dfrab3  4272  cocnvcnv2  6262  fmptap  7174  cnvoprab  8063  fpar  8117  fodomr  9123  fodomfir  9294  jech9.3  9793  dju1dif  10172  alephadd  10577  distrnq  10961  ltanq  10971  ltrnq  10979  1p2e3  12398  halfpm6th  12481  numma  12776  numaddc  12780  6p5lem  12802  8p2e10  12812  binom2i  14266  faclbnd4lem1  14347  cats2cat  14923  0.999...  15958  flodddiv4  16495  6gcd4e2  16618  dfphi2  16855  mod2xnegi  17153  karatsuba  17165  1259lem1  17213  setc2obas  18173  oppgtopn  19467  symgplusg  19497  cmnbascntr  19919  mgptopn  20268  ply1plusg  22433  ply1vsca  22434  ply1mulr  22435  restcld  23379  cmpsublem  23606  kgentopon  23746  dfii5  25095  itg1climres  25924  pigt3  26734  ang180lem1  27025  1cubrlem  27057  quart1lem  27071  efiatan  27128  log2cnv  27160  log2ublem3  27164  1sgm2ppw  27415  ppiub  27419  bposlem8  27506  bposlem9  27507  2lgsoddprmlem3c  27627  2lgsoddprmlem3d  27628  bday1  28058  addsasslem2  28248  seqsval  28532  ax5seglem7  29340  wlknwwlksnbij  30304  2pthd  30356  3pthd  30596  ipidsq  31133  ipdirilem  31252  norm3difi  31570  polid2i  31580  pjclem3  32620  cvmdi  32747  indifundif  32941  dpmul  33302  tocyccntz  33528  ccfldextdgrr  34126  cos9thpiminplylem5  34240  eulerpartlemt  34826  eulerpart  34837  ballotlem1  34942  ballotlemfval0  34951  ballotth  34993  hgt750lem  35103  hgt750lem2  35104  subfaclim  35717  kur14lem6  35740  quad3  36199  iexpire  36264  volsupnfl  38373  dfxrn2  39092  dmxrn  39094  dmxrnuncnvepres  39099  xrninxp  39122  1p3e4  43084  ipiiie0  43257  sn-0tie0  43283  areaquad  44001  wallispilem4  46840  dirkertrigeqlem3  46872  dirkercncflem1  46875  fourierswlem  47002  fouriersw  47003  smflimsuplem8  47599  ceil5half3  48141  3exp4mod41  48426  41prothprm  48429  tgoldbachlt  48639  zlmodzxz0  49193  linevalexample  49232  mndtcco  50420