Theorem 3eqtr2i 2792

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 2789	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2786	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  indif  4228  dfrab3  4267  cocnvcnv2  6279  fmptap  7206  cnvoprab  8106  fpar  8164  fodomr  9185  fodomfir  9357  jech9.3OLD  9860  dju1dif  10290  alephadd  10701  distrnq  11085  ltanq  11095  ltrnq  11103  1p2e3  12525  halfpm6th  12608  numma  12903  numaddc  12907  6p5lem  12929  8p2e10  12939  binom2i  14397  faclbnd4lem1  14478  cats2cat  15055  0.999...  16094  flodddiv4  16629  6gcd4e2  16755  dfphi2  16995  mod2xnegi  17293  karatsuba  17305  1259lem1  17353  setc2obas  18319  oppgtopn  19618  symgplusg  19648  cmnbascntr  20070  mgptopn  20419  ply1plusg  22596  ply1vsca  22597  ply1mulr  22598  restcld  23545  cmpsublem  23772  kgentopon  23912  dfii5  25261  itg1climres  26090  pigt3  26903  ang180lem1  27194  1cubrlem  27226  quart1lem  27240  efiatan  27297  log2cnv  27329  log2ublem3  27333  1sgm2ppw  27584  ppiub  27588  bposlem8  27675  bposlem9  27676  2lgsoddprmlem3c  27796  2lgsoddprmlem3d  27797  bday1  28257  addsasslem2  28447  seqsval  28731  ax5seglem7  29570  wlknwwlksnbij  30534  2pthd  30586  3pthd  30832  ipidsq  31369  ipdirilem  31488  norm3difi  31806  polid2i  31816  pjclem3  32856  cvmdi  32983  indifundif  33219  dpmul  33575  tocyccntz  33804  ccfldextdgrr  34415  cos9thpiminplylem5  34529  eulerpartlemt  35114  eulerpart  35125  ballotlem1  35230  ballotlemfval0  35239  ballotth  35281  hgt750lem  35391  hgt750lem2  35392  subfaclim  36161  kur14lem6  36184  quad3  36643  iexpire  36715  volsupnfl  38851  dfxrn2  39583  dmxrn  39585  dmxrnuncnvepres  39590  xrninxp  39613  1p3e4  43576  1p4e5  43577  1p5e6  43578  1p6e7  43579  1p7e8  43580  1p8e9  43581  4p5e9  43590  ipiiie0  43755  sn-0tie0  43781  areaquad  44479  wallispilem4  47351  dirkertrigeqlem3  47383  dirkercncflem1  47386  fourierswlem  47513  fouriersw  47514  smflimsuplem8  48110  goldpolyfactor  48200  ceil5half3  48689  3exp4mod41  48974  41prothprm  48977  tgoldbachlt  49187  bru3sqbru  49757  zlmodzxz0  49799  linevalexample  49838  mndtcco  51054