Theorem addcl 11209

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   + caddc 11130

This theorem was proved from axioms:  ax-addcl 11187

This theorem is referenced by:  mpoaddf  11221  adddir  11224  0cn  11225  addcli  11239  addcld  11252  muladd11  11403  peano2cn  11405  muladd11r  11446  add4  11454  0cnALT2  11469  negeu  11470  pncan  11486  2addsub  11494  addsubeq4  11495  nppcan2  11512  pnpcan  11520  ppncan  11523  muladd  11667  mulsub  11678  recex  11867  muleqadd  11879  conjmul  11956  halfaddsubcl  12471  halfaddsub  12472  serf  14046  seradd  14060  sersub  14061  binom3  14240  bernneq  14245  lswccatn0lsw  14607  revccat  14782  2cshwcshw  14842  shftlem  15085  shftval2  15092  shftval5  15095  2shfti  15097  crre  15131  crim  15132  cjadd  15158  addcj  15165  sqabsadd  15299  absreimsq  15309  absreim  15310  abstri  15347  sqreulem  15376  sqreu  15377  addcn2  15608  o1add  15628  climadd  15646  clim2ser  15669  clim2ser2  15670  isermulc2  15672  isercolllem3  15681  summolem3  15728  summolem2a  15729  fsumcl  15747  fsummulc2  15798  fsumrelem  15821  binom  15844  isumsplit  15854  risefacval2  16024  risefaccl  16029  risefallfac  16038  risefacp1  16043  binomfallfac  16055  binomrisefac  16056  bpoly3  16072  efcj  16106  ef4p  16129  tanval3  16150  efi4p  16153  sinadd  16180  cosadd  16181  tanadd  16183  addsin  16186  demoivreALT  16217  opoe  16380  pythagtriplem4  16837  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  gzaddcl  16955  cnaddablx  19847  cnaddabl  19848  cncrng  21349  cncrngOLD  21350  cnperf  24758  cnlmod  25089  cnstrcvs  25090  cncvs  25094  dvaddbr  25890  dvaddf  25895  dveflem  25933  plyaddcl  26175  plymulcl  26176  plysubcl  26177  coeaddlem  26204  dgrcolem1  26229  dgrcolem2  26230  quotlem  26258  quotcl2  26260  quotdgr  26261  sinperlem  26439  ptolemy  26455  tangtx  26464  sinkpi  26481  efif1olem2  26502  logrnaddcl  26533  logneg  26547  logimul  26573  cxpadd  26638  binom4  26810  atanf  26840  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsublem  26875  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  cosatan  26881  cosatanne0  26882  atantan  26883  atanbndlem  26885  atans2  26891  dvatan  26895  atantayl  26897  efrlim  26929  efrlimOLD  26930  dfef2  26931  gamcvg2lem  27019  ftalem7  27039  prmorcht  27138  bposlem9  27253  lgsquad2lem1  27345  2sqlem2  27379  cncph  30746  hhssnv  31191  hoadddir  31731  superpos  32281  knoppcnlem8  36464  cos2h  37581  tan2h  37582  ftc1anclem3  37665  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  facp2  42102  fac2xp3  42198  sumcubes  42309  fsumsermpt  45556  stirlinglem5  46055  stirlinglem7  46057  cnapbmcpd  47272  fmtnodvds  47506  opoeALTV  47645  mogoldbblem  47682