Theorem addcl 11152

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   + caddc 11073

This theorem was proved from axioms:  ax-addcl 11130

This theorem is referenced by:  mpoaddf  11164  adddir  11167  0cn  11168  addcli  11185  addcld  11198  muladd11  11350  peano2cn  11352  muladd11r  11393  add4  11401  0cnALT2  11416  negeu  11417  pncan  11433  2addsub  11441  addsubeq4  11442  nppcan2  11459  pnpcan  11467  ppncan  11470  muladd  11616  mulsub  11627  recex  11816  muleqadd  11828  conjmul  11905  halfaddsubcl  12450  halfaddsub  12451  serf  14040  seradd  14054  sersub  14055  binom3  14234  bernneq  14239  lswccatn0lsw  14602  revccat  14776  2cshwcshw  14835  shftlem  15078  shftval2  15085  shftval5  15088  2shfti  15090  crre  15124  crim  15125  cjadd  15151  addcj  15158  sqabsadd  15292  absreimsq  15302  absreim  15303  abstri  15341  sqreulem  15370  sqreu  15371  addcn2  15604  o1add  15624  climadd  15642  clim2ser  15665  clim2ser2  15666  isermulc2  15668  isercolllem3  15677  summolem3  15724  summolem2a  15725  fsumcl  15743  fsummulc2  15794  fsumrelem  15818  binom  15843  isumsplit  15853  risefacval2  16023  risefaccl  16028  risefallfac  16037  risefacp1  16042  binomfallfac  16054  binomrisefac  16055  bpoly3  16071  efcj  16105  ef4p  16128  tanval3  16149  efi4p  16152  sinadd  16179  cosadd  16180  tanadd  16182  addsin  16185  demoivreALT  16216  opoe  16380  pythagtriplem4  16838  pythagtriplem12  16845  pythagtriplem14  16847  pythagtriplem16  16849  gzaddcl  16956  cnaddablx  19891  cnaddabl  19892  cncrng  21425  cnperf  24861  cnlmod  25182  cnstrcvs  25183  cncvs  25187  dvaddbr  25980  dvaddf  25984  dveflem  26021  plyaddcl  26260  plymulcl  26261  plysubcl  26262  coeaddlem  26289  dgrcolem1  26313  dgrcolem2  26314  quotlem  26341  quotcl2  26343  quotdgr  26344  sinperlem  26522  ptolemy  26538  tangtx  26547  sinkpi  26564  efif1olem2  26585  logrnaddcl  26616  logneg  26630  logimul  26656  cxpadd  26721  binom4  26892  atanf  26922  atanneg  26949  atancj  26952  efiatan  26954  atanlogaddlem  26955  atanlogadd  26956  atanlogsublem  26957  atanlogsub  26958  efiatan2  26959  2efiatan  26960  tanatan  26961  cosatan  26963  cosatanne0  26964  atantan  26965  atanbndlem  26967  atans2  26973  dvatan  26977  atantayl  26979  efrlim  27011  dfef2  27012  gamcvg2lem  27100  ftalem7  27120  prmorcht  27219  bposlem9  27333  lgsquad2lem1  27425  2sqlem2  27459  cncph  30968  hhssnv  31413  hoadddir  31953  superpos  32503  knoppcnlem8  36902  cos2h  38074  tan2h  38075  ftc1anclem3  38158  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  facp2  42724  sumcubes  42886  fsumsermpt  46119  stirlinglem5  46616  stirlinglem7  46618  cnapbmcpd  47853  fmtnodvds  48117  opoeALTV  48269  mogoldbblem  48306