Theorem addcl 11266

Description: Alias for ax-addcl 11244, for naming consistency with addcli 11296. Use this theorem instead of ax-addcl 11244 or axaddcl 11220. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcl

Step	Hyp	Ref	Expression
1		ax-addcl 11244	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187

This theorem was proved from axioms:  ax-addcl 11244

This theorem is referenced by:  mpoaddf  11278  adddir  11281  0cn  11282  addcli  11296  addcld  11309  muladd11  11460  peano2cn  11462  muladd11r  11503  add4  11510  0cnALT2  11525  negeu  11526  pncan  11542  2addsub  11550  addsubeq4  11551  nppcan2  11567  pnpcan  11575  ppncan  11578  muladd  11722  mulsub  11733  recex  11922  muleqadd  11934  conjmul  12011  halfaddsubcl  12525  halfaddsub  12526  serf  14081  seradd  14095  sersub  14096  binom3  14273  bernneq  14278  lswccatn0lsw  14639  revccat  14814  2cshwcshw  14874  shftlem  15117  shftval2  15124  shftval5  15127  2shfti  15129  crre  15163  crim  15164  cjadd  15190  addcj  15197  sqabsadd  15331  absreimsq  15341  absreim  15342  abstri  15379  sqreulem  15408  sqreu  15409  addcn2  15640  o1add  15660  climadd  15678  clim2ser  15703  clim2ser2  15704  isermulc2  15706  isercolllem3  15715  summolem3  15762  summolem2a  15763  fsumcl  15781  fsummulc2  15832  fsumrelem  15855  binom  15878  isumsplit  15888  risefacval2  16058  risefaccl  16063  risefallfac  16072  risefacp1  16077  binomfallfac  16089  binomrisefac  16090  bpoly3  16106  efcj  16140  ef4p  16161  tanval3  16182  efi4p  16185  sinadd  16212  cosadd  16213  tanadd  16215  addsin  16218  demoivreALT  16249  opoe  16411  pythagtriplem4  16866  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem16  16877  gzaddcl  16984  cnaddablx  19910  cnaddabl  19911  cncrng  21424  cncrngOLD  21425  cnperf  24861  cnlmod  25192  cnstrcvs  25193  cncvs  25197  dvaddbr  25994  dvaddf  25999  dveflem  26037  plyaddcl  26279  plymulcl  26280  plysubcl  26281  coeaddlem  26308  dgrcolem1  26333  dgrcolem2  26334  quotlem  26360  quotcl2  26362  quotdgr  26363  sinperlem  26540  ptolemy  26556  tangtx  26565  sinkpi  26582  efif1olem2  26603  logrnaddcl  26634  logneg  26648  logimul  26674  cxpadd  26739  binom4  26911  atanf  26941  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  cosatan  26982  cosatanne0  26983  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl  26998  efrlim  27030  efrlimOLD  27031  dfef2  27032  gamcvg2lem  27120  ftalem7  27140  prmorcht  27239  bposlem9  27354  lgsquad2lem1  27446  2sqlem2  27480  cncph  30851  hhssnv  31296  hoadddir  31836  superpos  32386  knoppcnlem8  36466  cos2h  37571  tan2h  37572  ftc1anclem3  37655  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  facp2  42100  fac2xp3  42196  sumcubes  42301  fsumsermpt  45500  stirlinglem5  45999  stirlinglem7  46001  cnapbmcpd  47210  fmtnodvds  47418  opoeALTV  47557  mogoldbblem  47594