Theorem addcl 10962

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   + caddc 10883

This theorem was proved from axioms:  ax-addcl 10940

This theorem is referenced by:  adddir  10975  0cn  10976  addcli  10990  addcld  11003  muladd11  11154  peano2cn  11156  muladd11r  11197  add4  11204  0cnALT2  11219  negeu  11220  pncan  11236  2addsub  11244  addsubeq4  11245  nppcan2  11261  pnpcan  11269  ppncan  11272  muladd  11416  mulsub  11427  recex  11616  muleqadd  11628  conjmul  11701  halfaddsubcl  12214  halfaddsub  12215  serf  13760  seradd  13774  sersub  13775  binom3  13948  bernneq  13953  lswccatn0lsw  14305  revccat  14488  2cshwcshw  14547  shftlem  14788  shftval2  14795  shftval5  14798  2shfti  14800  crre  14834  crim  14835  cjadd  14861  addcj  14868  sqabsadd  15003  absreimsq  15013  absreim  15014  abstri  15051  sqreulem  15080  sqreu  15081  addcn2  15312  o1add  15332  climadd  15350  clim2ser  15375  clim2ser2  15376  isermulc2  15378  isercolllem3  15387  summolem3  15435  summolem2a  15436  fsumcl  15454  fsummulc2  15505  fsumrelem  15528  binom  15551  isumsplit  15561  risefacval2  15729  risefaccl  15734  risefallfac  15743  risefacp1  15748  binomfallfac  15760  binomrisefac  15761  bpoly3  15777  efcj  15810  ef4p  15831  tanval3  15852  efi4p  15855  sinadd  15882  cosadd  15883  tanadd  15885  addsin  15888  demoivreALT  15919  opoe  16081  pythagtriplem4  16529  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem16  16540  gzaddcl  16647  cnaddablx  19478  cnaddabl  19479  cncrng  20628  cnperf  23992  cnlmod  24312  cnstrcvs  24313  cncvs  24317  dvaddbr  25111  dvaddf  25115  dveflem  25152  plyaddcl  25390  plymulcl  25391  plysubcl  25392  coeaddlem  25419  dgrcolem1  25443  dgrcolem2  25444  quotlem  25469  quotcl2  25471  quotdgr  25472  sinperlem  25646  ptolemy  25662  tangtx  25671  sinkpi  25687  efif1olem2  25708  logrnaddcl  25739  logneg  25752  logimul  25778  cxpadd  25843  binom4  26009  atanf  26039  atanneg  26066  atancj  26069  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsublem  26074  atanlogsub  26075  efiatan2  26076  2efiatan  26077  tanatan  26078  cosatan  26080  cosatanne0  26081  atantan  26082  atanbndlem  26084  atans2  26090  dvatan  26094  atantayl  26096  efrlim  26128  dfef2  26129  gamcvg2lem  26217  ftalem7  26237  prmorcht  26336  bposlem9  26449  lgsquad2lem1  26541  2sqlem2  26575  cncph  29190  hhssnv  29635  hoadddir  30175  superpos  30725  knoppcnlem8  34689  cos2h  35777  tan2h  35778  ftc1anclem3  35861  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  facp2  40106  fac2xp3  40167  fsumsermpt  43127  stirlinglem5  43626  stirlinglem7  43628  cnapbmcpd  44798  fmtnodvds  45007  opoeALTV  45146  mogoldbblem  45183