Theorem addcl 11237

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158

This theorem was proved from axioms:  ax-addcl 11215

This theorem is referenced by:  mpoaddf  11249  adddir  11252  0cn  11253  addcli  11267  addcld  11280  muladd11  11431  peano2cn  11433  muladd11r  11474  add4  11482  0cnALT2  11497  negeu  11498  pncan  11514  2addsub  11522  addsubeq4  11523  nppcan2  11540  pnpcan  11548  ppncan  11551  muladd  11695  mulsub  11706  recex  11895  muleqadd  11907  conjmul  11984  halfaddsubcl  12498  halfaddsub  12499  serf  14071  seradd  14085  sersub  14086  binom3  14263  bernneq  14268  lswccatn0lsw  14629  revccat  14804  2cshwcshw  14864  shftlem  15107  shftval2  15114  shftval5  15117  2shfti  15119  crre  15153  crim  15154  cjadd  15180  addcj  15187  sqabsadd  15321  absreimsq  15331  absreim  15332  abstri  15369  sqreulem  15398  sqreu  15399  addcn2  15630  o1add  15650  climadd  15668  clim2ser  15691  clim2ser2  15692  isermulc2  15694  isercolllem3  15703  summolem3  15750  summolem2a  15751  fsumcl  15769  fsummulc2  15820  fsumrelem  15843  binom  15866  isumsplit  15876  risefacval2  16046  risefaccl  16051  risefallfac  16060  risefacp1  16065  binomfallfac  16077  binomrisefac  16078  bpoly3  16094  efcj  16128  ef4p  16149  tanval3  16170  efi4p  16173  sinadd  16200  cosadd  16201  tanadd  16203  addsin  16206  demoivreALT  16237  opoe  16400  pythagtriplem4  16857  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  gzaddcl  16975  cnaddablx  19886  cnaddabl  19887  cncrng  21401  cncrngOLD  21402  cnperf  24842  cnlmod  25173  cnstrcvs  25174  cncvs  25178  dvaddbr  25974  dvaddf  25979  dveflem  26017  plyaddcl  26259  plymulcl  26260  plysubcl  26261  coeaddlem  26288  dgrcolem1  26313  dgrcolem2  26314  quotlem  26342  quotcl2  26344  quotdgr  26345  sinperlem  26522  ptolemy  26538  tangtx  26547  sinkpi  26564  efif1olem2  26585  logrnaddcl  26616  logneg  26630  logimul  26656  cxpadd  26721  binom4  26893  atanf  26923  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsublem  26958  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  cosatan  26964  cosatanne0  26965  atantan  26966  atanbndlem  26968  atans2  26974  dvatan  26978  atantayl  26980  efrlim  27012  efrlimOLD  27013  dfef2  27014  gamcvg2lem  27102  ftalem7  27122  prmorcht  27221  bposlem9  27336  lgsquad2lem1  27428  2sqlem2  27462  cncph  30838  hhssnv  31283  hoadddir  31823  superpos  32373  knoppcnlem8  36501  cos2h  37618  tan2h  37619  ftc1anclem3  37702  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  facp2  42144  fac2xp3  42240  sumcubes  42347  fsumsermpt  45594  stirlinglem5  46093  stirlinglem7  46095  cnapbmcpd  47307  fmtnodvds  47531  opoeALTV  47670  mogoldbblem  47707