Theorem addcl 11118

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039

This theorem was proved from axioms:  ax-addcl 11096

This theorem is referenced by:  mpoaddf  11130  adddir  11133  0cn  11134  addcli  11149  addcld  11162  muladd11  11314  peano2cn  11316  muladd11r  11357  add4  11365  0cnALT2  11380  negeu  11381  pncan  11397  2addsub  11405  addsubeq4  11406  nppcan2  11423  pnpcan  11431  ppncan  11434  muladd  11580  mulsub  11591  recex  11780  muleqadd  11792  conjmul  11870  halfaddsubcl  12407  halfaddsub  12408  serf  13990  seradd  14004  sersub  14005  binom3  14184  bernneq  14189  lswccatn0lsw  14552  revccat  14726  2cshwcshw  14785  shftlem  15028  shftval2  15035  shftval5  15038  2shfti  15040  crre  15074  crim  15075  cjadd  15101  addcj  15108  sqabsadd  15242  absreimsq  15252  absreim  15253  abstri  15291  sqreulem  15320  sqreu  15321  addcn2  15554  o1add  15574  climadd  15592  clim2ser  15615  clim2ser2  15616  isermulc2  15618  isercolllem3  15627  summolem3  15674  summolem2a  15675  fsumcl  15693  fsummulc2  15744  fsumrelem  15768  binom  15793  isumsplit  15803  risefacval2  15973  risefaccl  15978  risefallfac  15987  risefacp1  15992  binomfallfac  16004  binomrisefac  16005  bpoly3  16021  efcj  16055  ef4p  16078  tanval3  16099  efi4p  16102  sinadd  16129  cosadd  16130  tanadd  16132  addsin  16135  demoivreALT  16166  opoe  16330  pythagtriplem4  16788  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem16  16799  gzaddcl  16906  cnaddablx  19841  cnaddabl  19842  cncrng  21375  cnperf  24811  cnlmod  25132  cnstrcvs  25133  cncvs  25137  dvaddbr  25930  dvaddf  25934  dveflem  25971  plyaddcl  26210  plymulcl  26211  plysubcl  26212  coeaddlem  26239  dgrcolem1  26263  dgrcolem2  26264  quotlem  26291  quotcl2  26293  quotdgr  26294  sinperlem  26469  ptolemy  26485  tangtx  26494  sinkpi  26511  efif1olem2  26532  logrnaddcl  26563  logneg  26577  logimul  26603  cxpadd  26668  binom4  26839  atanf  26869  atanneg  26896  atancj  26899  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsublem  26904  atanlogsub  26905  efiatan2  26906  2efiatan  26907  tanatan  26908  cosatan  26910  cosatanne0  26911  atantan  26912  atanbndlem  26914  atans2  26920  dvatan  26924  atantayl  26926  efrlim  26958  dfef2  26959  gamcvg2lem  27047  ftalem7  27067  prmorcht  27166  bposlem9  27280  lgsquad2lem1  27372  2sqlem2  27406  cncph  30915  hhssnv  31360  hoadddir  31900  superpos  32450  knoppcnlem8  36813  cos2h  37985  tan2h  37986  ftc1anclem3  38069  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  facp2  42635  sumcubes  42797  fsumsermpt  46031  stirlinglem5  46528  stirlinglem7  46530  cnapbmcpd  47765  fmtnodvds  48029  opoeALTV  48181  mogoldbblem  48218