Theorem addcl 10884

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805

This theorem was proved from axioms:  ax-addcl 10862

This theorem is referenced by:  adddir  10897  0cn  10898  addcli  10912  addcld  10925  muladd11  11075  peano2cn  11077  muladd11r  11118  add4  11125  0cnALT2  11140  negeu  11141  pncan  11157  2addsub  11165  addsubeq4  11166  nppcan2  11182  pnpcan  11190  ppncan  11193  muladd  11337  mulsub  11348  recex  11537  muleqadd  11549  conjmul  11622  halfaddsubcl  12135  halfaddsub  12136  serf  13679  seradd  13693  sersub  13694  binom3  13867  bernneq  13872  lswccatn0lsw  14224  revccat  14407  2cshwcshw  14466  shftlem  14707  shftval2  14714  shftval5  14717  2shfti  14719  crre  14753  crim  14754  cjadd  14780  addcj  14787  sqabsadd  14922  absreimsq  14932  absreim  14933  abstri  14970  sqreulem  14999  sqreu  15000  addcn2  15231  o1add  15251  climadd  15269  clim2ser  15294  clim2ser2  15295  isermulc2  15297  isercolllem3  15306  summolem3  15354  summolem2a  15355  fsumcl  15373  fsummulc2  15424  fsumrelem  15447  binom  15470  isumsplit  15480  risefacval2  15648  risefaccl  15653  risefallfac  15662  risefacp1  15667  binomfallfac  15679  binomrisefac  15680  bpoly3  15696  efcj  15729  ef4p  15750  tanval3  15771  efi4p  15774  sinadd  15801  cosadd  15802  tanadd  15804  addsin  15807  demoivreALT  15838  opoe  16000  pythagtriplem4  16448  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  gzaddcl  16566  cnaddablx  19384  cnaddabl  19385  cncrng  20531  cnperf  23889  cnlmod  24209  cnstrcvs  24210  cncvs  24214  dvaddbr  25007  dvaddf  25011  dveflem  25048  plyaddcl  25286  plymulcl  25287  plysubcl  25288  coeaddlem  25315  dgrcolem1  25339  dgrcolem2  25340  quotlem  25365  quotcl2  25367  quotdgr  25368  sinperlem  25542  ptolemy  25558  tangtx  25567  sinkpi  25583  efif1olem2  25604  logrnaddcl  25635  logneg  25648  logimul  25674  cxpadd  25739  binom4  25905  atanf  25935  atanneg  25962  atancj  25965  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsublem  25970  atanlogsub  25971  efiatan2  25972  2efiatan  25973  tanatan  25974  cosatan  25976  cosatanne0  25977  atantan  25978  atanbndlem  25980  atans2  25986  dvatan  25990  atantayl  25992  efrlim  26024  dfef2  26025  gamcvg2lem  26113  ftalem7  26133  prmorcht  26232  bposlem9  26345  lgsquad2lem1  26437  2sqlem2  26471  cncph  29082  hhssnv  29527  hoadddir  30067  superpos  30617  knoppcnlem8  34607  cos2h  35695  tan2h  35696  ftc1anclem3  35779  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  facp2  40027  fac2xp3  40088  fsumsermpt  43010  stirlinglem5  43509  stirlinglem7  43511  cnapbmcpd  44675  fmtnodvds  44884  opoeALTV  45023  mogoldbblem  45060