Theorem addcl 11157

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078

This theorem was proved from axioms:  ax-addcl 11135

This theorem is referenced by:  mpoaddf  11169  adddir  11172  0cn  11173  addcli  11187  addcld  11200  muladd11  11351  peano2cn  11353  muladd11r  11394  add4  11402  0cnALT2  11417  negeu  11418  pncan  11434  2addsub  11442  addsubeq4  11443  nppcan2  11460  pnpcan  11468  ppncan  11471  muladd  11617  mulsub  11628  recex  11817  muleqadd  11829  conjmul  11906  halfaddsubcl  12421  halfaddsub  12422  serf  14002  seradd  14016  sersub  14017  binom3  14196  bernneq  14201  lswccatn0lsw  14563  revccat  14738  2cshwcshw  14798  shftlem  15041  shftval2  15048  shftval5  15051  2shfti  15053  crre  15087  crim  15088  cjadd  15114  addcj  15121  sqabsadd  15255  absreimsq  15265  absreim  15266  abstri  15304  sqreulem  15333  sqreu  15334  addcn2  15567  o1add  15587  climadd  15605  clim2ser  15628  clim2ser2  15629  isermulc2  15631  isercolllem3  15640  summolem3  15687  summolem2a  15688  fsumcl  15706  fsummulc2  15757  fsumrelem  15780  binom  15803  isumsplit  15813  risefacval2  15983  risefaccl  15988  risefallfac  15997  risefacp1  16002  binomfallfac  16014  binomrisefac  16015  bpoly3  16031  efcj  16065  ef4p  16088  tanval3  16109  efi4p  16112  sinadd  16139  cosadd  16140  tanadd  16142  addsin  16145  demoivreALT  16176  opoe  16340  pythagtriplem4  16797  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  gzaddcl  16915  cnaddablx  19805  cnaddabl  19806  cncrng  21307  cncrngOLD  21308  cnperf  24716  cnlmod  25047  cnstrcvs  25048  cncvs  25052  dvaddbr  25847  dvaddf  25852  dveflem  25890  plyaddcl  26132  plymulcl  26133  plysubcl  26134  coeaddlem  26161  dgrcolem1  26186  dgrcolem2  26187  quotlem  26215  quotcl2  26217  quotdgr  26218  sinperlem  26396  ptolemy  26412  tangtx  26421  sinkpi  26438  efif1olem2  26459  logrnaddcl  26490  logneg  26504  logimul  26530  cxpadd  26595  binom4  26767  atanf  26797  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  cosatan  26838  cosatanne0  26839  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  efrlim  26886  efrlimOLD  26887  dfef2  26888  gamcvg2lem  26976  ftalem7  26996  prmorcht  27095  bposlem9  27210  lgsquad2lem1  27302  2sqlem2  27336  cncph  30755  hhssnv  31200  hoadddir  31740  superpos  32290  knoppcnlem8  36495  cos2h  37612  tan2h  37613  ftc1anclem3  37696  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  facp2  42138  sumcubes  42308  fsumsermpt  45584  stirlinglem5  46083  stirlinglem7  46085  cnapbmcpd  47300  fmtnodvds  47549  opoeALTV  47688  mogoldbblem  47725