Theorem addcl 11110

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031

This theorem was proved from axioms:  ax-addcl 11088

This theorem is referenced by:  mpoaddf  11122  adddir  11125  0cn  11126  addcli  11140  addcld  11153  muladd11  11304  peano2cn  11306  muladd11r  11347  add4  11355  0cnALT2  11370  negeu  11371  pncan  11387  2addsub  11395  addsubeq4  11396  nppcan2  11413  pnpcan  11421  ppncan  11424  muladd  11570  mulsub  11581  recex  11770  muleqadd  11782  conjmul  11859  halfaddsubcl  12374  halfaddsub  12375  serf  13955  seradd  13969  sersub  13970  binom3  14149  bernneq  14154  lswccatn0lsw  14516  revccat  14690  2cshwcshw  14750  shftlem  14993  shftval2  15000  shftval5  15003  2shfti  15005  crre  15039  crim  15040  cjadd  15066  addcj  15073  sqabsadd  15207  absreimsq  15217  absreim  15218  abstri  15256  sqreulem  15285  sqreu  15286  addcn2  15519  o1add  15539  climadd  15557  clim2ser  15580  clim2ser2  15581  isermulc2  15583  isercolllem3  15592  summolem3  15639  summolem2a  15640  fsumcl  15658  fsummulc2  15709  fsumrelem  15732  binom  15755  isumsplit  15765  risefacval2  15935  risefaccl  15940  risefallfac  15949  risefacp1  15954  binomfallfac  15966  binomrisefac  15967  bpoly3  15983  efcj  16017  ef4p  16040  tanval3  16061  efi4p  16064  sinadd  16091  cosadd  16092  tanadd  16094  addsin  16097  demoivreALT  16128  opoe  16292  pythagtriplem4  16749  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  gzaddcl  16867  cnaddablx  19765  cnaddabl  19766  cncrng  21313  cncrngOLD  21314  cnperf  24725  cnlmod  25056  cnstrcvs  25057  cncvs  25061  dvaddbr  25856  dvaddf  25861  dveflem  25899  plyaddcl  26141  plymulcl  26142  plysubcl  26143  coeaddlem  26170  dgrcolem1  26195  dgrcolem2  26196  quotlem  26224  quotcl2  26226  quotdgr  26227  sinperlem  26405  ptolemy  26421  tangtx  26430  sinkpi  26447  efif1olem2  26468  logrnaddcl  26499  logneg  26513  logimul  26539  cxpadd  26604  binom4  26776  atanf  26806  atanneg  26833  atancj  26836  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsublem  26841  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  cosatan  26847  cosatanne0  26848  atantan  26849  atanbndlem  26851  atans2  26857  dvatan  26861  atantayl  26863  efrlim  26895  efrlimOLD  26896  dfef2  26897  gamcvg2lem  26985  ftalem7  27005  prmorcht  27104  bposlem9  27219  lgsquad2lem1  27311  2sqlem2  27345  cncph  30781  hhssnv  31226  hoadddir  31766  superpos  32316  knoppcnlem8  36473  cos2h  37590  tan2h  37591  ftc1anclem3  37674  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  facp2  42116  sumcubes  42286  fsumsermpt  45561  stirlinglem5  46060  stirlinglem7  46062  cnapbmcpd  47280  fmtnodvds  47529  opoeALTV  47668  mogoldbblem  47705