Theorem addcl 11120

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041

This theorem was proved from axioms:  ax-addcl 11098

This theorem is referenced by:  mpoaddf  11132  adddir  11135  0cn  11136  addcli  11150  addcld  11163  muladd11  11315  peano2cn  11317  muladd11r  11358  add4  11366  0cnALT2  11381  negeu  11382  pncan  11398  2addsub  11406  addsubeq4  11407  nppcan2  11424  pnpcan  11432  ppncan  11435  muladd  11581  mulsub  11592  recex  11781  muleqadd  11793  conjmul  11870  halfaddsubcl  12385  halfaddsub  12386  serf  13965  seradd  13979  sersub  13980  binom3  14159  bernneq  14164  lswccatn0lsw  14527  revccat  14701  2cshwcshw  14760  shftlem  15003  shftval2  15010  shftval5  15013  2shfti  15015  crre  15049  crim  15050  cjadd  15076  addcj  15083  sqabsadd  15217  absreimsq  15227  absreim  15228  abstri  15266  sqreulem  15295  sqreu  15296  addcn2  15529  o1add  15549  climadd  15567  clim2ser  15590  clim2ser2  15591  isermulc2  15593  isercolllem3  15602  summolem3  15649  summolem2a  15650  fsumcl  15668  fsummulc2  15719  fsumrelem  15742  binom  15765  isumsplit  15775  risefacval2  15945  risefaccl  15950  risefallfac  15959  risefacp1  15964  binomfallfac  15976  binomrisefac  15977  bpoly3  15993  efcj  16027  ef4p  16050  tanval3  16071  efi4p  16074  sinadd  16101  cosadd  16102  tanadd  16104  addsin  16107  demoivreALT  16138  opoe  16302  pythagtriplem4  16759  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  gzaddcl  16877  cnaddablx  19809  cnaddabl  19810  cncrng  21355  cncrngOLD  21356  cnperf  24777  cnlmod  25108  cnstrcvs  25109  cncvs  25113  dvaddbr  25908  dvaddf  25913  dveflem  25951  plyaddcl  26193  plymulcl  26194  plysubcl  26195  coeaddlem  26222  dgrcolem1  26247  dgrcolem2  26248  quotlem  26276  quotcl2  26278  quotdgr  26279  sinperlem  26457  ptolemy  26473  tangtx  26482  sinkpi  26499  efif1olem2  26520  logrnaddcl  26551  logneg  26565  logimul  26591  cxpadd  26656  binom4  26828  atanf  26858  atanneg  26885  atancj  26888  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsublem  26893  atanlogsub  26894  efiatan2  26895  2efiatan  26896  tanatan  26897  cosatan  26899  cosatanne0  26900  atantan  26901  atanbndlem  26903  atans2  26909  dvatan  26913  atantayl  26915  efrlim  26947  efrlimOLD  26948  dfef2  26949  gamcvg2lem  27037  ftalem7  27057  prmorcht  27156  bposlem9  27271  lgsquad2lem1  27363  2sqlem2  27397  cncph  30906  hhssnv  31351  hoadddir  31891  superpos  32441  knoppcnlem8  36719  cos2h  37856  tan2h  37857  ftc1anclem3  37940  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  facp2  42507  sumcubes  42677  fsumsermpt  45933  stirlinglem5  46430  stirlinglem7  46432  cnapbmcpd  47649  fmtnodvds  47898  opoeALTV  48037  mogoldbblem  48074