Theorem addcl 11120

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

This theorem was proved from axioms:  ax-addcl 11098

This theorem is referenced by:  mpoaddf  11132  adddir  11135  0cn  11136  addcli  11151  addcld  11164  muladd11  11316  peano2cn  11318  muladd11r  11359  add4  11367  0cnALT2  11382  negeu  11383  pncan  11399  2addsub  11407  addsubeq4  11408  nppcan2  11425  pnpcan  11433  ppncan  11436  muladd  11582  mulsub  11593  recex  11782  muleqadd  11794  conjmul  11872  halfaddsubcl  12409  halfaddsub  12410  serf  13992  seradd  14006  sersub  14007  binom3  14186  bernneq  14191  lswccatn0lsw  14554  revccat  14728  2cshwcshw  14787  shftlem  15030  shftval2  15037  shftval5  15040  2shfti  15042  crre  15076  crim  15077  cjadd  15103  addcj  15110  sqabsadd  15244  absreimsq  15254  absreim  15255  abstri  15293  sqreulem  15322  sqreu  15323  addcn2  15556  o1add  15576  climadd  15594  clim2ser  15617  clim2ser2  15618  isermulc2  15620  isercolllem3  15629  summolem3  15676  summolem2a  15677  fsumcl  15695  fsummulc2  15746  fsumrelem  15770  binom  15795  isumsplit  15805  risefacval2  15975  risefaccl  15980  risefallfac  15989  risefacp1  15994  binomfallfac  16006  binomrisefac  16007  bpoly3  16023  efcj  16057  ef4p  16080  tanval3  16101  efi4p  16104  sinadd  16131  cosadd  16132  tanadd  16134  addsin  16137  demoivreALT  16168  opoe  16332  pythagtriplem4  16790  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  gzaddcl  16908  cnaddablx  19843  cnaddabl  19844  cncrng  21373  cnperf  24786  cnlmod  25107  cnstrcvs  25108  cncvs  25112  dvaddbr  25905  dvaddf  25909  dveflem  25946  plyaddcl  26185  plymulcl  26186  plysubcl  26187  coeaddlem  26214  dgrcolem1  26238  dgrcolem2  26239  quotlem  26266  quotcl2  26268  quotdgr  26269  sinperlem  26444  ptolemy  26460  tangtx  26469  sinkpi  26486  efif1olem2  26507  logrnaddcl  26538  logneg  26552  logimul  26578  cxpadd  26643  binom4  26814  atanf  26844  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsublem  26879  atanlogsub  26880  efiatan2  26881  2efiatan  26882  tanatan  26883  cosatan  26885  cosatanne0  26886  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  efrlim  26933  dfef2  26934  gamcvg2lem  27022  ftalem7  27042  prmorcht  27141  bposlem9  27255  lgsquad2lem1  27347  2sqlem2  27381  cncph  30890  hhssnv  31335  hoadddir  31875  superpos  32425  knoppcnlem8  36760  cos2h  37932  tan2h  37933  ftc1anclem3  38016  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  facp2  42582  sumcubes  42745  fsumsermpt  46009  stirlinglem5  46506  stirlinglem7  46508  cnapbmcpd  47743  fmtnodvds  48007  opoeALTV  48159  mogoldbblem  48196