Theorem addcl 11183

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104

This theorem was proved from axioms:  ax-addcl 11161

This theorem is referenced by:  mpoaddf  11195  adddir  11198  0cn  11199  addcli  11216  addcld  11229  muladd11  11381  peano2cn  11383  muladd11r  11424  add4  11432  0cnALT2  11447  negeu  11448  pncan  11464  2addsub  11472  addsubeq4  11473  nppcan2  11490  pnpcan  11498  ppncan  11501  muladd  11647  mulsub  11658  recex  11847  muleqadd  11859  conjmul  11933  halfaddsubcl  12477  halfaddsub  12478  serf  14068  seradd  14082  sersub  14083  binom3  14262  bernneq  14267  lswccatn0lsw  14631  revccat  14805  2cshwcshw  14864  shftlem  15107  shftval2  15114  shftval5  15117  2shfti  15119  crre  15167  crim  15168  cjadd  15194  addcj  15201  sqabsadd  15335  absreimsq  15345  absreim  15346  abstri  15384  sqreulem  15413  sqreu  15414  addcn2  15647  o1add  15667  climadd  15685  clim2ser  15708  clim2ser2  15709  isermulc2  15711  isercolllem3  15720  summolem3  15767  summolem2a  15768  fsumcl  15786  fsummulc2  15837  fsumrelem  15861  binom  15886  isumsplit  15896  risefacval2  16066  risefaccl  16071  risefallfac  16080  risefacp1  16084  binomfallfac  16096  binomrisefac  16097  bpoly3  16113  efcj  16147  ef4p  16170  tanval3  16191  efi4p  16194  sinadd  16221  cosadd  16222  tanadd  16224  addsin  16227  demoivreALT  16258  opoe  16422  pythagtriplem4  16880  pythagtriplem12  16887  pythagtriplem14  16889  pythagtriplem16  16891  gzaddcl  16998  cnaddablx  19939  cnaddabl  19940  cncrng  21524  cnperf  24959  cnlmod  25280  cnstrcvs  25281  cncvs  25285  dvaddbr  26078  dvaddf  26082  dveflem  26119  plyaddcl  26358  plymulcl  26359  plysubcl  26360  coeaddlem  26387  dgrcolem1  26411  dgrcolem2  26412  quotlem  26442  quotcl2  26444  quotdgr  26445  sinperlem  26623  ptolemy  26639  tangtx  26648  sinkpi  26665  efif1olem2  26686  logrnaddcl  26717  logneg  26731  logimul  26757  cxpadd  26822  binom4  26993  atanf  27023  atanneg  27050  atancj  27053  efiatan  27055  atanlogaddlem  27056  atanlogadd  27057  atanlogsublem  27058  atanlogsub  27059  efiatan2  27060  2efiatan  27061  tanatan  27062  cosatan  27064  cosatanne0  27065  atantan  27066  atanbndlem  27068  atans2  27074  dvatan  27078  atantayl  27080  efrlim  27112  dfef2  27113  gamcvg2lem  27201  ftalem7  27221  prmorcht  27320  bposlem9  27434  lgsquad2lem1  27526  2sqlem2  27560  cncph  31149  hhssnv  31594  hoadddir  32134  superpos  32684  knoppcnlem8  37067  cos2h  38240  tan2h  38241  ftc1anclem3  38324  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  facp2  42888  sumcubes  43052  fsumsermpt  46275  stirlinglem5  46772  stirlinglem7  46774  cnapbmcpd  48009  fmtnodvds  48273  opoeALTV  48425  mogoldbblem  48462