Theorem addcl 9897

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

This theorem was proved from axioms:  ax-addcl 9875

This theorem is referenced by:  adddir  9910  0cn  9911  addcli  9923  addcld  9938  muladd11  10085  peano2cn  10087  muladd11r  10128  add4  10135  0cnALT  10149  negeu  10150  pncan  10166  2addsub  10174  addsubeq4  10175  nppcan2  10191  ppncan  10202  muladd  10341  mulsub  10352  recex  10538  muleqadd  10550  conjmul  10621  halfaddsubcl  11141  halfaddsub  11142  serf  12691  seradd  12705  sersub  12706  binom3  12847  bernneq  12852  lswccatn0lsw  13226  revccat  13366  2cshwcshw  13422  shftlem  13656  shftval2  13663  shftval5  13666  2shfti  13668  crre  13702  crim  13703  cjadd  13729  addcj  13736  sqabsadd  13870  absreimsq  13880  absreim  13881  abstri  13918  sqreulem  13947  sqreu  13948  addcn2  14172  o1add  14192  climadd  14210  clim2ser  14233  clim2ser2  14234  isermulc2  14236  isercolllem3  14245  summolem3  14292  summolem2a  14293  fsumcl  14311  fsummulc2  14358  fsumrelem  14380  binom  14401  isumsplit  14411  risefacval2  14580  risefaccl  14585  risefallfac  14594  risefacp1  14599  binomfallfac  14611  binomrisefac  14612  bpoly3  14628  efcj  14661  ef4p  14682  tanval3  14703  efi4p  14706  sinadd  14733  cosadd  14734  tanadd  14736  addsin  14739  demoivreALT  14770  opoe  14925  pythagtriplem4  15362  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  gzaddcl  15479  cnaddablx  18094  cnaddabl  18095  cncrng  19586  cnperf  22431  cnlmod  22748  cnstrcvs  22749  cncvs  22753  dvaddbr  23507  dvaddf  23511  dveflem  23546  plyaddcl  23780  plymulcl  23781  plysubcl  23782  coeaddlem  23809  dgrcolem1  23833  dgrcolem2  23834  quotlem  23859  quotcl2  23861  quotdgr  23862  sinperlem  24036  ptolemy  24052  tangtx  24061  sinkpi  24075  efif1olem2  24093  logrnaddcl  24125  logneg  24138  logimul  24164  cxpadd  24225  binom4  24377  atanf  24407  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  cosatan  24448  cosatanne0  24449  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  efrlim  24496  dfef2  24497  gamcvg2lem  24585  ftalem7  24605  prmorcht  24704  bposlem9  24817  lgsquad2lem1  24909  2sqlem2  24943  wlkdvspthlem  26137  wwlkext2clwwlk  26331  cncph  27058  hhssnv  27505  hoadddir  28047  superpos  28597  knoppcnlem8  31660  cos2h  32570  tan2h  32571  ftc1anclem3  32657  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  fsumsermpt  38646  stirlinglem5  38971  stirlinglem7  38973  fmtnodvds  39994  opoeALTV  40132  cnapbmcpd  40342  wwlksext2clwwlk  41231