Theorem addcl 11170

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091

This theorem was proved from axioms:  ax-addcl 11148

This theorem is referenced by:  mpoaddf  11182  adddir  11185  0cn  11186  addcli  11203  addcld  11216  muladd11  11368  peano2cn  11370  muladd11r  11411  add4  11419  0cnALT2  11434  negeu  11435  pncan  11451  2addsub  11459  addsubeq4  11460  nppcan2  11477  pnpcan  11485  ppncan  11488  muladd  11634  mulsub  11645  recex  11834  muleqadd  11846  conjmul  11923  halfaddsubcl  12467  halfaddsub  12468  serf  14057  seradd  14071  sersub  14072  binom3  14251  bernneq  14256  lswccatn0lsw  14619  revccat  14793  2cshwcshw  14852  shftlem  15095  shftval2  15102  shftval5  15105  2shfti  15107  crre  15155  crim  15156  cjadd  15182  addcj  15189  sqabsadd  15323  absreimsq  15333  absreim  15334  abstri  15372  sqreulem  15401  sqreu  15402  addcn2  15635  o1add  15655  climadd  15673  clim2ser  15696  clim2ser2  15697  isermulc2  15699  isercolllem3  15708  summolem3  15755  summolem2a  15756  fsumcl  15774  fsummulc2  15825  fsumrelem  15849  binom  15874  isumsplit  15884  risefacval2  16054  risefaccl  16059  risefallfac  16068  risefacp1  16073  binomfallfac  16085  binomrisefac  16086  bpoly3  16102  efcj  16136  ef4p  16159  tanval3  16180  efi4p  16183  sinadd  16210  cosadd  16211  tanadd  16213  addsin  16216  demoivreALT  16247  opoe  16411  pythagtriplem4  16869  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem16  16880  gzaddcl  16987  cnaddablx  19929  cnaddabl  19930  cncrng  21503  cnperf  24939  cnlmod  25260  cnstrcvs  25261  cncvs  25265  dvaddbr  26058  dvaddf  26062  dveflem  26099  plyaddcl  26338  plymulcl  26339  plysubcl  26340  coeaddlem  26367  dgrcolem1  26391  dgrcolem2  26392  quotlem  26422  quotcl2  26424  quotdgr  26425  sinperlem  26603  ptolemy  26619  tangtx  26628  sinkpi  26645  efif1olem2  26666  logrnaddcl  26697  logneg  26711  logimul  26737  cxpadd  26802  binom4  26973  atanf  27003  atanneg  27030  atancj  27033  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsublem  27038  atanlogsub  27039  efiatan2  27040  2efiatan  27041  tanatan  27042  cosatan  27044  cosatanne0  27045  atantan  27046  atanbndlem  27048  atans2  27054  dvatan  27058  atantayl  27060  efrlim  27092  dfef2  27093  gamcvg2lem  27181  ftalem7  27201  prmorcht  27300  bposlem9  27414  lgsquad2lem1  27506  2sqlem2  27540  cncph  31080  hhssnv  31525  hoadddir  32065  superpos  32615  knoppcnlem8  36951  cos2h  38122  tan2h  38123  ftc1anclem3  38206  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  facp2  42772  sumcubes  42934  fsumsermpt  46153  stirlinglem5  46650  stirlinglem7  46652  cnapbmcpd  47887  fmtnodvds  48151  opoeALTV  48303  mogoldbblem  48340