Theorem addcl 10018

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934   + caddc 9939

This theorem was proved from axioms:  ax-addcl 9996

This theorem is referenced by:  adddir  10031  0cn  10032  addcli  10044  addcld  10059  muladd11  10206  peano2cn  10208  muladd11r  10249  add4  10256  0cnALT  10270  negeu  10271  pncan  10287  2addsub  10295  addsubeq4  10296  nppcan2  10312  ppncan  10323  muladd  10462  mulsub  10473  recex  10659  muleqadd  10671  conjmul  10742  halfaddsubcl  11264  halfaddsub  11265  serf  12829  seradd  12843  sersub  12844  binom3  12985  bernneq  12990  lswccatn0lsw  13373  revccat  13515  2cshwcshw  13571  shftlem  13808  shftval2  13815  shftval5  13818  2shfti  13820  crre  13854  crim  13855  cjadd  13881  addcj  13888  sqabsadd  14022  absreimsq  14032  absreim  14033  abstri  14070  sqreulem  14099  sqreu  14100  addcn2  14324  o1add  14344  climadd  14362  clim2ser  14385  clim2ser2  14386  isermulc2  14388  isercolllem3  14397  summolem3  14445  summolem2a  14446  fsumcl  14464  fsummulc2  14516  fsumrelem  14539  binom  14562  isumsplit  14572  risefacval2  14741  risefaccl  14746  risefallfac  14755  risefacp1  14760  binomfallfac  14772  binomrisefac  14773  bpoly3  14789  efcj  14822  ef4p  14843  tanval3  14864  efi4p  14867  sinadd  14894  cosadd  14895  tanadd  14897  addsin  14900  demoivreALT  14931  opoe  15087  pythagtriplem4  15524  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  gzaddcl  15641  cnaddablx  18271  cnaddabl  18272  cncrng  19767  cnperf  22623  cnlmod  22940  cnstrcvs  22941  cncvs  22945  dvaddbr  23701  dvaddf  23705  dveflem  23742  plyaddcl  23976  plymulcl  23977  plysubcl  23978  coeaddlem  24005  dgrcolem1  24029  dgrcolem2  24030  quotlem  24055  quotcl2  24057  quotdgr  24058  sinperlem  24232  ptolemy  24248  tangtx  24257  sinkpi  24271  efif1olem2  24289  logrnaddcl  24321  logneg  24334  logimul  24360  cxpadd  24425  binom4  24577  atanf  24607  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  cosatan  24648  cosatanne0  24649  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  efrlim  24696  dfef2  24697  gamcvg2lem  24785  ftalem7  24805  prmorcht  24904  bposlem9  25017  lgsquad2lem1  25109  2sqlem2  25143  wwlksext2clwwlk  26924  cncph  27674  hhssnv  28121  hoadddir  28663  superpos  29213  knoppcnlem8  32490  cos2h  33400  tan2h  33401  ftc1anclem3  33487  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  fsumsermpt  39811  stirlinglem5  40295  stirlinglem7  40297  cnapbmcpd  41310  fmtnodvds  41456  opoeALTV  41594  mogoldbblem  41629