Theorem addcl 11234

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155

This theorem was proved from axioms:  ax-addcl 11212

This theorem is referenced by:  mpoaddf  11246  adddir  11249  0cn  11250  addcli  11264  addcld  11277  muladd11  11428  peano2cn  11430  muladd11r  11471  add4  11479  0cnALT2  11494  negeu  11495  pncan  11511  2addsub  11519  addsubeq4  11520  nppcan2  11537  pnpcan  11545  ppncan  11548  muladd  11692  mulsub  11703  recex  11892  muleqadd  11904  conjmul  11981  halfaddsubcl  12495  halfaddsub  12496  serf  14067  seradd  14081  sersub  14082  binom3  14259  bernneq  14264  lswccatn0lsw  14625  revccat  14800  2cshwcshw  14860  shftlem  15103  shftval2  15110  shftval5  15113  2shfti  15115  crre  15149  crim  15150  cjadd  15176  addcj  15183  sqabsadd  15317  absreimsq  15327  absreim  15328  abstri  15365  sqreulem  15394  sqreu  15395  addcn2  15626  o1add  15646  climadd  15664  clim2ser  15687  clim2ser2  15688  isermulc2  15690  isercolllem3  15699  summolem3  15746  summolem2a  15747  fsumcl  15765  fsummulc2  15816  fsumrelem  15839  binom  15862  isumsplit  15872  risefacval2  16042  risefaccl  16047  risefallfac  16056  risefacp1  16061  binomfallfac  16073  binomrisefac  16074  bpoly3  16090  efcj  16124  ef4p  16145  tanval3  16166  efi4p  16169  sinadd  16196  cosadd  16197  tanadd  16199  addsin  16202  demoivreALT  16233  opoe  16396  pythagtriplem4  16852  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  gzaddcl  16970  cnaddablx  19900  cnaddabl  19901  cncrng  21418  cncrngOLD  21419  cnperf  24855  cnlmod  25186  cnstrcvs  25187  cncvs  25191  dvaddbr  25988  dvaddf  25993  dveflem  26031  plyaddcl  26273  plymulcl  26274  plysubcl  26275  coeaddlem  26302  dgrcolem1  26327  dgrcolem2  26328  quotlem  26356  quotcl2  26358  quotdgr  26359  sinperlem  26536  ptolemy  26552  tangtx  26561  sinkpi  26578  efif1olem2  26599  logrnaddcl  26630  logneg  26644  logimul  26670  cxpadd  26735  binom4  26907  atanf  26937  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  cosatan  26978  cosatanne0  26979  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  efrlim  27026  efrlimOLD  27027  dfef2  27028  gamcvg2lem  27116  ftalem7  27136  prmorcht  27235  bposlem9  27350  lgsquad2lem1  27442  2sqlem2  27476  cncph  30847  hhssnv  31292  hoadddir  31832  superpos  32382  knoppcnlem8  36482  cos2h  37597  tan2h  37598  ftc1anclem3  37681  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  facp2  42124  fac2xp3  42220  sumcubes  42325  fsumsermpt  45534  stirlinglem5  46033  stirlinglem7  46035  cnapbmcpd  47244  fmtnodvds  47468  opoeALTV  47607  mogoldbblem  47644