Theorem addcl 11098

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   + caddc 11019

This theorem was proved from axioms:  ax-addcl 11076

This theorem is referenced by:  mpoaddf  11110  adddir  11113  0cn  11114  addcli  11128  addcld  11141  muladd11  11293  peano2cn  11295  muladd11r  11336  add4  11344  0cnALT2  11359  negeu  11360  pncan  11376  2addsub  11384  addsubeq4  11385  nppcan2  11402  pnpcan  11410  ppncan  11413  muladd  11559  mulsub  11570  recex  11759  muleqadd  11771  conjmul  11848  halfaddsubcl  12363  halfaddsub  12364  serf  13947  seradd  13961  sersub  13962  binom3  14141  bernneq  14146  lswccatn0lsw  14509  revccat  14683  2cshwcshw  14742  shftlem  14985  shftval2  14992  shftval5  14995  2shfti  14997  crre  15031  crim  15032  cjadd  15058  addcj  15065  sqabsadd  15199  absreimsq  15209  absreim  15210  abstri  15248  sqreulem  15277  sqreu  15278  addcn2  15511  o1add  15531  climadd  15549  clim2ser  15572  clim2ser2  15573  isermulc2  15575  isercolllem3  15584  summolem3  15631  summolem2a  15632  fsumcl  15650  fsummulc2  15701  fsumrelem  15724  binom  15747  isumsplit  15757  risefacval2  15927  risefaccl  15932  risefallfac  15941  risefacp1  15946  binomfallfac  15958  binomrisefac  15959  bpoly3  15975  efcj  16009  ef4p  16032  tanval3  16053  efi4p  16056  sinadd  16083  cosadd  16084  tanadd  16086  addsin  16089  demoivreALT  16120  opoe  16284  pythagtriplem4  16741  pythagtriplem12  16748  pythagtriplem14  16750  pythagtriplem16  16752  gzaddcl  16859  cnaddablx  19790  cnaddabl  19791  cncrng  21335  cncrngOLD  21336  cnperf  24746  cnlmod  25077  cnstrcvs  25078  cncvs  25082  dvaddbr  25877  dvaddf  25882  dveflem  25920  plyaddcl  26162  plymulcl  26163  plysubcl  26164  coeaddlem  26191  dgrcolem1  26216  dgrcolem2  26217  quotlem  26245  quotcl2  26247  quotdgr  26248  sinperlem  26426  ptolemy  26442  tangtx  26451  sinkpi  26468  efif1olem2  26489  logrnaddcl  26520  logneg  26534  logimul  26560  cxpadd  26625  binom4  26797  atanf  26827  atanneg  26854  atancj  26857  efiatan  26859  atanlogaddlem  26860  atanlogadd  26861  atanlogsublem  26862  atanlogsub  26863  efiatan2  26864  2efiatan  26865  tanatan  26866  cosatan  26868  cosatanne0  26869  atantan  26870  atanbndlem  26872  atans2  26878  dvatan  26882  atantayl  26884  efrlim  26916  efrlimOLD  26917  dfef2  26918  gamcvg2lem  27006  ftalem7  27026  prmorcht  27125  bposlem9  27240  lgsquad2lem1  27332  2sqlem2  27366  cncph  30810  hhssnv  31255  hoadddir  31795  superpos  32345  knoppcnlem8  36555  cos2h  37661  tan2h  37662  ftc1anclem3  37745  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  facp2  42246  sumcubes  42421  fsumsermpt  45693  stirlinglem5  46190  stirlinglem7  46192  cnapbmcpd  47409  fmtnodvds  47658  opoeALTV  47797  mogoldbblem  47834