Theorem addcl 10611

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108  (class class class)co 7148  ℂcc 10527   + caddc 10532

This theorem was proved from axioms:  ax-addcl 10589

This theorem is referenced by:  adddir  10624  0cn  10625  addcli  10639  addcld  10652  muladd11  10802  peano2cn  10804  muladd11r  10845  add4  10852  0cnALT2  10867  negeu  10868  pncan  10884  2addsub  10892  addsubeq4  10893  nppcan2  10909  pnpcan  10917  ppncan  10920  muladd  11064  mulsub  11075  recex  11264  muleqadd  11276  conjmul  11349  halfaddsubcl  11861  halfaddsub  11862  serf  13390  seradd  13404  sersub  13405  binom3  13577  bernneq  13582  lswccatn0lsw  13937  revccat  14120  2cshwcshw  14179  shftlem  14419  shftval2  14426  shftval5  14429  2shfti  14431  crre  14465  crim  14466  cjadd  14492  addcj  14499  sqabsadd  14634  absreimsq  14644  absreim  14645  abstri  14682  sqreulem  14711  sqreu  14712  addcn2  14942  o1add  14962  climadd  14980  clim2ser  15003  clim2ser2  15004  isermulc2  15006  isercolllem3  15015  summolem3  15063  summolem2a  15064  fsumcl  15082  fsummulc2  15131  fsumrelem  15154  binom  15177  isumsplit  15187  risefacval2  15356  risefaccl  15361  risefallfac  15370  risefacp1  15375  binomfallfac  15387  binomrisefac  15388  bpoly3  15404  efcj  15437  ef4p  15458  tanval3  15479  efi4p  15482  sinadd  15509  cosadd  15510  tanadd  15512  addsin  15515  demoivreALT  15546  opoe  15704  pythagtriplem4  16148  pythagtriplem12  16155  pythagtriplem14  16157  pythagtriplem16  16159  gzaddcl  16265  cnaddablx  18980  cnaddabl  18981  cncrng  20558  cnperf  23420  cnlmod  23736  cnstrcvs  23737  cncvs  23741  dvaddbr  24527  dvaddf  24531  dveflem  24568  plyaddcl  24802  plymulcl  24803  plysubcl  24804  coeaddlem  24831  dgrcolem1  24855  dgrcolem2  24856  quotlem  24881  quotcl2  24883  quotdgr  24884  sinperlem  25058  ptolemy  25074  tangtx  25083  sinkpi  25099  efif1olem2  25119  logrnaddcl  25150  logneg  25163  logimul  25189  cxpadd  25254  binom4  25420  atanf  25450  atanneg  25477  atancj  25480  efiatan  25482  atanlogaddlem  25483  atanlogadd  25484  atanlogsublem  25485  atanlogsub  25486  efiatan2  25487  2efiatan  25488  tanatan  25489  cosatan  25491  cosatanne0  25492  atantan  25493  atanbndlem  25495  atans2  25501  dvatan  25505  atantayl  25507  efrlim  25539  dfef2  25540  gamcvg2lem  25628  ftalem7  25648  prmorcht  25747  bposlem9  25860  lgsquad2lem1  25952  2sqlem2  25986  cncph  28588  hhssnv  29033  hoadddir  29573  superpos  30123  knoppcnlem8  33832  cos2h  34875  tan2h  34876  ftc1anclem3  34961  ftc1anclem7  34965  ftc1anclem8  34966  ftc1anc  34967  fsumsermpt  41849  stirlinglem5  42353  stirlinglem7  42355  cnapbmcpd  43485  fmtnodvds  43696  opoeALTV  43838  mogoldbblem  43875