Theorem addcl 11263

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   + caddc 11184

This proof depends on axioms:  ax-addcl 11241

This theorem is used by:  mpoaddf  11275  adddir  11278  0cn  11279  addcli  11296  addcld  11309  muladd11  11461  peano2cn  11463  muladd11r  11504  add4  11512  0cnALT2  11527  negeu  11528  pncan  11544  2addsub  11552  addsubeq4  11553  nppcan2  11570  pnpcan  11578  ppncan  11581  muladd  11729  mulsub  11740  recex  11929  muleqadd  11941  conjmul  12015  halfaddsubcl  12559  halfaddsub  12560  serf  14153  seradd  14167  sersub  14168  binom3  14348  bernneq  14353  lswccatn0lsw  14718  revccat  14895  2cshwcshw  14956  shftlem  15201  shftval2  15208  shftval5  15211  2shfti  15213  crre  15261  crim  15262  cjadd  15288  addcj  15295  sqabsadd  15429  absreimsq  15439  absreim  15440  abstri  15478  sqreulem  15507  sqreu  15508  addcn2  15741  o1add  15761  climadd  15779  clim2ser  15802  clim2ser2  15803  isermulc2  15805  isercolllem3  15814  summolem3  15860  summolem2a  15861  fsumcl  15879  fsummulc2  15930  fsumrelem  15954  binom  15979  isumsplit  15989  risefacval2  16157  risefaccl  16162  risefallfac  16171  risefacp1  16175  binomfallfac  16187  binomrisefac  16188  bpoly3  16204  efcj  16238  ef4p  16261  tanval3  16282  efi4p  16285  sinadd  16312  cosadd  16313  tanadd  16315  addsin  16318  demoivreALT  16349  opoe  16513  pythagtriplem4  16977  pythagtriplem12  16984  pythagtriplem14  16986  pythagtriplem16  16988  gzaddcl  17095  cnaddablx  20062  cnaddabl  20063  cncrng  21679  cnperf  25120  cnlmod  25441  cnstrcvs  25442  cncvs  25446  dvaddbr  26238  dvaddf  26242  dveflem  26279  plyaddcl  26519  plymulcl  26520  plysubcl  26521  coeaddlem  26548  dgrcolem1  26572  dgrcolem2  26573  quotlem  26603  quotcl2  26605  quotdgr  26606  sinperlem  26791  ptolemy  26807  tangtx  26816  sinkpi  26832  efif1olem2  26853  logrnaddcl  26884  logneg  26898  logimul  26924  cxpadd  26989  binom4  27160  atanf  27190  atanneg  27217  atancj  27220  efiatan  27222  atanlogaddlem  27223  atanlogadd  27224  atanlogsublem  27225  atanlogsub  27226  efiatan2  27227  2efiatan  27228  tanatan  27229  cosatan  27231  cosatanne0  27232  atantan  27233  atanbndlem  27235  atans2  27241  dvatan  27245  atantayl  27247  efrlim  27279  dfef2  27280  gamcvg2lem  27368  ftalem7  27388  prmorcht  27487  bposlem9  27601  lgsquad2lem1  27693  2sqlem2  27727  cncph  31403  hhssnv  31848  hoadddir  32388  superpos  32938  knoppcnlem8  37336  cos2h  38502  tan2h  38503  ftc1anclem3  38581  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  facp2  43161  sumcubes  43338  fsumsermpt  46535  stirlinglem5  47032  stirlinglem7  47034  cnapbmcpd  48309  fmtnodvds  48573  opoeALTV  48725  mogoldbblem  48762