Theorem addcl 11309

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   + caddc 11230

This proof depends on axioms:  ax-addcl 11287

This theorem is used by:  mpoaddf  11321  adddir  11324  0cn  11325  addcli  11342  addcld  11355  muladd11  11507  peano2cn  11509  muladd11r  11550  add4  11558  0cnALT2  11573  negeu  11574  pncan  11590  2addsub  11598  addsubeq4  11599  nppcan2  11616  pnpcan  11624  ppncan  11627  muladd  11775  mulsub  11786  recex  11975  muleqadd  11987  conjmul  12061  halfaddsubcl  12605  halfaddsub  12606  serf  14200  seradd  14214  sersub  14215  binom3  14395  bernneq  14400  lswccatn0lsw  14765  revccat  14943  2cshwcshw  15004  shftlem  15250  shftval2  15257  shftval5  15260  2shfti  15262  crre  15310  crim  15311  cjadd  15337  addcj  15344  sqabsadd  15478  absreimsq  15488  absreim  15489  abstri  15527  sqreulem  15556  sqreu  15557  addcn2  15790  o1add  15810  climadd  15828  clim2ser  15851  clim2ser2  15852  isermulc2  15854  isercolllem3  15863  summolem3  15909  summolem2a  15910  fsumcl  15928  fsummulc2  15979  fsumrelem  16003  binom  16028  isumsplit  16038  risefacval2  16206  risefaccl  16211  risefallfac  16220  risefacp1  16224  binomfallfac  16236  binomrisefac  16237  bpoly3  16253  efcj  16287  ef4p  16310  tanval3  16331  efi4p  16334  sinadd  16361  cosadd  16362  tanadd  16364  addsin  16367  demoivreALT  16398  opoe  16562  pythagtriplem4  17026  pythagtriplem12  17033  pythagtriplem14  17035  pythagtriplem16  17037  gzaddcl  17144  cnaddablx  20112  cnaddabl  20113  cncrng  21729  cnperf  25170  cnlmod  25491  cnstrcvs  25492  cncvs  25496  dvaddbr  26288  dvaddf  26292  dveflem  26329  plyaddcl  26569  plymulcl  26570  plysubcl  26571  coeaddlem  26598  dgrcolem1  26622  dgrcolem2  26623  quotlem  26651  quotcl2  26653  quotdgr  26654  sinperlem  26839  ptolemy  26855  tangtx  26864  sinkpi  26880  efif1olem2  26901  logrnaddcl  26932  logneg  26946  logimul  26972  cxpadd  27037  binom4  27208  atanf  27238  atanneg  27265  atancj  27268  efiatan  27270  atanlogaddlem  27271  atanlogadd  27272  atanlogsublem  27273  atanlogsub  27274  efiatan2  27275  2efiatan  27276  tanatan  27277  cosatan  27279  cosatanne0  27280  atantan  27281  atanbndlem  27283  atans2  27289  dvatan  27293  atantayl  27295  efrlim  27327  dfef2  27328  gamcvg2lem  27416  ftalem7  27436  prmorcht  27535  bposlem9  27649  lgsquad2lem1  27741  2sqlem2  27775  cncph  31451  hhssnv  31896  hoadddir  32436  superpos  32986  knoppcnlem8  37544  cos2h  38726  tan2h  38727  ftc1anclem3  38805  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  facp2  43385  sumcubes  43563  fsumsermpt  46796  stirlinglem5  47293  stirlinglem7  47295  cnapbmcpd  48570  fmtnodvds  48834  opoeALTV  48986  mogoldbblem  49023