Theorem addcl 11150

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071

This theorem was proved from axioms:  ax-addcl 11128

This theorem is referenced by:  mpoaddf  11162  adddir  11165  0cn  11166  addcli  11180  addcld  11193  muladd11  11344  peano2cn  11346  muladd11r  11387  add4  11395  0cnALT2  11410  negeu  11411  pncan  11427  2addsub  11435  addsubeq4  11436  nppcan2  11453  pnpcan  11461  ppncan  11464  muladd  11610  mulsub  11621  recex  11810  muleqadd  11822  conjmul  11899  halfaddsubcl  12414  halfaddsub  12415  serf  13995  seradd  14009  sersub  14010  binom3  14189  bernneq  14194  lswccatn0lsw  14556  revccat  14731  2cshwcshw  14791  shftlem  15034  shftval2  15041  shftval5  15044  2shfti  15046  crre  15080  crim  15081  cjadd  15107  addcj  15114  sqabsadd  15248  absreimsq  15258  absreim  15259  abstri  15297  sqreulem  15326  sqreu  15327  addcn2  15560  o1add  15580  climadd  15598  clim2ser  15621  clim2ser2  15622  isermulc2  15624  isercolllem3  15633  summolem3  15680  summolem2a  15681  fsumcl  15699  fsummulc2  15750  fsumrelem  15773  binom  15796  isumsplit  15806  risefacval2  15976  risefaccl  15981  risefallfac  15990  risefacp1  15995  binomfallfac  16007  binomrisefac  16008  bpoly3  16024  efcj  16058  ef4p  16081  tanval3  16102  efi4p  16105  sinadd  16132  cosadd  16133  tanadd  16135  addsin  16138  demoivreALT  16169  opoe  16333  pythagtriplem4  16790  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  gzaddcl  16908  cnaddablx  19798  cnaddabl  19799  cncrng  21300  cncrngOLD  21301  cnperf  24709  cnlmod  25040  cnstrcvs  25041  cncvs  25045  dvaddbr  25840  dvaddf  25845  dveflem  25883  plyaddcl  26125  plymulcl  26126  plysubcl  26127  coeaddlem  26154  dgrcolem1  26179  dgrcolem2  26180  quotlem  26208  quotcl2  26210  quotdgr  26211  sinperlem  26389  ptolemy  26405  tangtx  26414  sinkpi  26431  efif1olem2  26452  logrnaddcl  26483  logneg  26497  logimul  26523  cxpadd  26588  binom4  26760  atanf  26790  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  cosatan  26831  cosatanne0  26832  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  efrlim  26879  efrlimOLD  26880  dfef2  26881  gamcvg2lem  26969  ftalem7  26989  prmorcht  27088  bposlem9  27203  lgsquad2lem1  27295  2sqlem2  27329  cncph  30748  hhssnv  31193  hoadddir  31733  superpos  32283  knoppcnlem8  36488  cos2h  37605  tan2h  37606  ftc1anclem3  37689  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  facp2  42131  sumcubes  42301  fsumsermpt  45577  stirlinglem5  46076  stirlinglem7  46078  cnapbmcpd  47296  fmtnodvds  47545  opoeALTV  47684  mogoldbblem  47721