Theorem addcl 11111

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032

This theorem was proved from axioms:  ax-addcl 11089

This theorem is referenced by:  mpoaddf  11123  adddir  11126  0cn  11127  addcli  11142  addcld  11155  muladd11  11307  peano2cn  11309  muladd11r  11350  add4  11358  0cnALT2  11373  negeu  11374  pncan  11390  2addsub  11398  addsubeq4  11399  nppcan2  11416  pnpcan  11424  ppncan  11427  muladd  11573  mulsub  11584  recex  11773  muleqadd  11785  conjmul  11863  halfaddsubcl  12400  halfaddsub  12401  serf  13983  seradd  13997  sersub  13998  binom3  14177  bernneq  14182  lswccatn0lsw  14545  revccat  14719  2cshwcshw  14778  shftlem  15021  shftval2  15028  shftval5  15031  2shfti  15033  crre  15067  crim  15068  cjadd  15094  addcj  15101  sqabsadd  15235  absreimsq  15245  absreim  15246  abstri  15284  sqreulem  15313  sqreu  15314  addcn2  15547  o1add  15567  climadd  15585  clim2ser  15608  clim2ser2  15609  isermulc2  15611  isercolllem3  15620  summolem3  15667  summolem2a  15668  fsumcl  15686  fsummulc2  15737  fsumrelem  15761  binom  15786  isumsplit  15796  risefacval2  15966  risefaccl  15971  risefallfac  15980  risefacp1  15985  binomfallfac  15997  binomrisefac  15998  bpoly3  16014  efcj  16048  ef4p  16071  tanval3  16092  efi4p  16095  sinadd  16122  cosadd  16123  tanadd  16125  addsin  16128  demoivreALT  16159  opoe  16323  pythagtriplem4  16781  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  gzaddcl  16899  cnaddablx  19834  cnaddabl  19835  cncrng  21378  cncrngOLD  21379  cnperf  24796  cnlmod  25117  cnstrcvs  25118  cncvs  25122  dvaddbr  25915  dvaddf  25919  dveflem  25956  plyaddcl  26195  plymulcl  26196  plysubcl  26197  coeaddlem  26224  dgrcolem1  26248  dgrcolem2  26249  quotlem  26277  quotcl2  26279  quotdgr  26280  sinperlem  26457  ptolemy  26473  tangtx  26482  sinkpi  26499  efif1olem2  26520  logrnaddcl  26551  logneg  26565  logimul  26591  cxpadd  26656  binom4  26827  atanf  26857  atanneg  26884  atancj  26887  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsublem  26892  atanlogsub  26893  efiatan2  26894  2efiatan  26895  tanatan  26896  cosatan  26898  cosatanne0  26899  atantan  26900  atanbndlem  26902  atans2  26908  dvatan  26912  atantayl  26914  efrlim  26946  efrlimOLD  26947  dfef2  26948  gamcvg2lem  27036  ftalem7  27056  prmorcht  27155  bposlem9  27269  lgsquad2lem1  27361  2sqlem2  27395  cncph  30905  hhssnv  31350  hoadddir  31890  superpos  32440  knoppcnlem8  36776  cos2h  37946  tan2h  37947  ftc1anclem3  38030  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  facp2  42596  sumcubes  42759  fsumsermpt  46027  stirlinglem5  46524  stirlinglem7  46526  cnapbmcpd  47755  fmtnodvds  48019  opoeALTV  48171  mogoldbblem  48208