Theorem addcl 11188

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  (class class class)co 7401  ℂcc 11104   + caddc 11109

This theorem was proved from axioms:  ax-addcl 11166

This theorem is referenced by:  adddir  11202  0cn  11203  addcli  11217  addcld  11230  muladd11  11381  peano2cn  11383  muladd11r  11424  add4  11431  0cnALT2  11446  negeu  11447  pncan  11463  2addsub  11471  addsubeq4  11472  nppcan2  11488  pnpcan  11496  ppncan  11499  muladd  11643  mulsub  11654  recex  11843  muleqadd  11855  conjmul  11928  halfaddsubcl  12441  halfaddsub  12442  serf  13993  seradd  14007  sersub  14008  binom3  14184  bernneq  14189  lswccatn0lsw  14538  revccat  14713  2cshwcshw  14773  shftlem  15012  shftval2  15019  shftval5  15022  2shfti  15024  crre  15058  crim  15059  cjadd  15085  addcj  15092  sqabsadd  15226  absreimsq  15236  absreim  15237  abstri  15274  sqreulem  15303  sqreu  15304  addcn2  15535  o1add  15555  climadd  15573  clim2ser  15598  clim2ser2  15599  isermulc2  15601  isercolllem3  15610  summolem3  15657  summolem2a  15658  fsumcl  15676  fsummulc2  15727  fsumrelem  15750  binom  15773  isumsplit  15783  risefacval2  15951  risefaccl  15956  risefallfac  15965  risefacp1  15970  binomfallfac  15982  binomrisefac  15983  bpoly3  15999  efcj  16032  ef4p  16053  tanval3  16074  efi4p  16077  sinadd  16104  cosadd  16105  tanadd  16107  addsin  16110  demoivreALT  16141  opoe  16303  pythagtriplem4  16751  pythagtriplem12  16758  pythagtriplem14  16760  pythagtriplem16  16762  gzaddcl  16869  cnaddablx  19778  cnaddabl  19779  cncrng  21250  cnperf  24658  cnlmod  24989  cnstrcvs  24990  cncvs  24994  dvaddbr  25790  dvaddf  25795  dveflem  25833  plyaddcl  26074  plymulcl  26075  plysubcl  26076  coeaddlem  26103  dgrcolem1  26128  dgrcolem2  26129  quotlem  26154  quotcl2  26156  quotdgr  26157  sinperlem  26332  ptolemy  26348  tangtx  26357  sinkpi  26373  efif1olem2  26394  logrnaddcl  26425  logneg  26438  logimul  26464  cxpadd  26529  binom4  26698  atanf  26728  atanneg  26755  atancj  26758  efiatan  26760  atanlogaddlem  26761  atanlogadd  26762  atanlogsublem  26763  atanlogsub  26764  efiatan2  26765  2efiatan  26766  tanatan  26767  cosatan  26769  cosatanne0  26770  atantan  26771  atanbndlem  26773  atans2  26779  dvatan  26783  atantayl  26785  efrlim  26817  efrlimOLD  26818  dfef2  26819  gamcvg2lem  26907  ftalem7  26927  prmorcht  27026  bposlem9  27141  lgsquad2lem1  27233  2sqlem2  27267  cncph  30541  hhssnv  30986  hoadddir  31526  superpos  32076  mpoaddf  35658  gg-cncrng  35673  knoppcnlem8  35866  cos2h  36969  tan2h  36970  ftc1anclem3  37053  ftc1anclem7  37057  ftc1anclem8  37058  ftc1anc  37059  facp2  41452  fac2xp3  41513  sumcubes  41700  fsumsermpt  44780  stirlinglem5  45279  stirlinglem7  45281  cnapbmcpd  46488  fmtnodvds  46697  opoeALTV  46836  mogoldbblem  46873