Theorem addcl 11095

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016

This theorem was proved from axioms:  ax-addcl 11073

This theorem is referenced by:  mpoaddf  11107  adddir  11110  0cn  11111  addcli  11125  addcld  11138  muladd11  11290  peano2cn  11292  muladd11r  11333  add4  11341  0cnALT2  11356  negeu  11357  pncan  11373  2addsub  11381  addsubeq4  11382  nppcan2  11399  pnpcan  11407  ppncan  11410  muladd  11556  mulsub  11567  recex  11756  muleqadd  11768  conjmul  11845  halfaddsubcl  12360  halfaddsub  12361  serf  13939  seradd  13953  sersub  13954  binom3  14133  bernneq  14138  lswccatn0lsw  14501  revccat  14675  2cshwcshw  14734  shftlem  14977  shftval2  14984  shftval5  14987  2shfti  14989  crre  15023  crim  15024  cjadd  15050  addcj  15057  sqabsadd  15191  absreimsq  15201  absreim  15202  abstri  15240  sqreulem  15269  sqreu  15270  addcn2  15503  o1add  15523  climadd  15541  clim2ser  15564  clim2ser2  15565  isermulc2  15567  isercolllem3  15576  summolem3  15623  summolem2a  15624  fsumcl  15642  fsummulc2  15693  fsumrelem  15716  binom  15739  isumsplit  15749  risefacval2  15919  risefaccl  15924  risefallfac  15933  risefacp1  15938  binomfallfac  15950  binomrisefac  15951  bpoly3  15967  efcj  16001  ef4p  16024  tanval3  16045  efi4p  16048  sinadd  16075  cosadd  16076  tanadd  16078  addsin  16081  demoivreALT  16112  opoe  16276  pythagtriplem4  16733  pythagtriplem12  16740  pythagtriplem14  16742  pythagtriplem16  16744  gzaddcl  16851  cnaddablx  19782  cnaddabl  19783  cncrng  21327  cncrngOLD  21328  cnperf  24737  cnlmod  25068  cnstrcvs  25069  cncvs  25073  dvaddbr  25868  dvaddf  25873  dveflem  25911  plyaddcl  26153  plymulcl  26154  plysubcl  26155  coeaddlem  26182  dgrcolem1  26207  dgrcolem2  26208  quotlem  26236  quotcl2  26238  quotdgr  26239  sinperlem  26417  ptolemy  26433  tangtx  26442  sinkpi  26459  efif1olem2  26480  logrnaddcl  26511  logneg  26525  logimul  26551  cxpadd  26616  binom4  26788  atanf  26818  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  cosatan  26859  cosatanne0  26860  atantan  26861  atanbndlem  26863  atans2  26869  dvatan  26873  atantayl  26875  efrlim  26907  efrlimOLD  26908  dfef2  26909  gamcvg2lem  26997  ftalem7  27017  prmorcht  27116  bposlem9  27231  lgsquad2lem1  27323  2sqlem2  27357  cncph  30801  hhssnv  31246  hoadddir  31786  superpos  32336  knoppcnlem8  36565  cos2h  37671  tan2h  37672  ftc1anclem3  37755  ftc1anclem7  37759  ftc1anclem8  37760  ftc1anc  37761  facp2  42256  sumcubes  42431  fsumsermpt  45703  stirlinglem5  46200  stirlinglem7  46202  cnapbmcpd  47419  fmtnodvds  47668  opoeALTV  47807  mogoldbblem  47844