Theorem addcl 11108

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029

This theorem was proved from axioms:  ax-addcl 11086

This theorem is referenced by:  mpoaddf  11120  adddir  11123  0cn  11124  addcli  11138  addcld  11151  muladd11  11303  peano2cn  11305  muladd11r  11346  add4  11354  0cnALT2  11369  negeu  11370  pncan  11386  2addsub  11394  addsubeq4  11395  nppcan2  11412  pnpcan  11420  ppncan  11423  muladd  11569  mulsub  11580  recex  11769  muleqadd  11781  conjmul  11858  halfaddsubcl  12373  halfaddsub  12374  serf  13953  seradd  13967  sersub  13968  binom3  14147  bernneq  14152  lswccatn0lsw  14515  revccat  14689  2cshwcshw  14748  shftlem  14991  shftval2  14998  shftval5  15001  2shfti  15003  crre  15037  crim  15038  cjadd  15064  addcj  15071  sqabsadd  15205  absreimsq  15215  absreim  15216  abstri  15254  sqreulem  15283  sqreu  15284  addcn2  15517  o1add  15537  climadd  15555  clim2ser  15578  clim2ser2  15579  isermulc2  15581  isercolllem3  15590  summolem3  15637  summolem2a  15638  fsumcl  15656  fsummulc2  15707  fsumrelem  15730  binom  15753  isumsplit  15763  risefacval2  15933  risefaccl  15938  risefallfac  15947  risefacp1  15952  binomfallfac  15964  binomrisefac  15965  bpoly3  15981  efcj  16015  ef4p  16038  tanval3  16059  efi4p  16062  sinadd  16089  cosadd  16090  tanadd  16092  addsin  16095  demoivreALT  16126  opoe  16290  pythagtriplem4  16747  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  gzaddcl  16865  cnaddablx  19797  cnaddabl  19798  cncrng  21343  cncrngOLD  21344  cnperf  24765  cnlmod  25096  cnstrcvs  25097  cncvs  25101  dvaddbr  25896  dvaddf  25901  dveflem  25939  plyaddcl  26181  plymulcl  26182  plysubcl  26183  coeaddlem  26210  dgrcolem1  26235  dgrcolem2  26236  quotlem  26264  quotcl2  26266  quotdgr  26267  sinperlem  26445  ptolemy  26461  tangtx  26470  sinkpi  26487  efif1olem2  26508  logrnaddcl  26539  logneg  26553  logimul  26579  cxpadd  26644  binom4  26816  atanf  26846  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsublem  26881  atanlogsub  26882  efiatan2  26883  2efiatan  26884  tanatan  26885  cosatan  26887  cosatanne0  26888  atantan  26889  atanbndlem  26891  atans2  26897  dvatan  26901  atantayl  26903  efrlim  26935  efrlimOLD  26936  dfef2  26937  gamcvg2lem  27025  ftalem7  27045  prmorcht  27144  bposlem9  27259  lgsquad2lem1  27351  2sqlem2  27385  cncph  30894  hhssnv  31339  hoadddir  31879  superpos  32429  knoppcnlem8  36700  cos2h  37808  tan2h  37809  ftc1anclem3  37892  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  facp2  42393  sumcubes  42564  fsumsermpt  45821  stirlinglem5  46318  stirlinglem7  46320  cnapbmcpd  47537  fmtnodvds  47786  opoeALTV  47925  mogoldbblem  47962