Theorem addcl 11085

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   + caddc 11006

This theorem was proved from axioms:  ax-addcl 11063

This theorem is referenced by:  mpoaddf  11097  adddir  11100  0cn  11101  addcli  11115  addcld  11128  muladd11  11280  peano2cn  11282  muladd11r  11323  add4  11331  0cnALT2  11346  negeu  11347  pncan  11363  2addsub  11371  addsubeq4  11372  nppcan2  11389  pnpcan  11397  ppncan  11400  muladd  11546  mulsub  11557  recex  11746  muleqadd  11758  conjmul  11835  halfaddsubcl  12350  halfaddsub  12351  serf  13934  seradd  13948  sersub  13949  binom3  14128  bernneq  14133  lswccatn0lsw  14496  revccat  14670  2cshwcshw  14729  shftlem  14972  shftval2  14979  shftval5  14982  2shfti  14984  crre  15018  crim  15019  cjadd  15045  addcj  15052  sqabsadd  15186  absreimsq  15196  absreim  15197  abstri  15235  sqreulem  15264  sqreu  15265  addcn2  15498  o1add  15518  climadd  15536  clim2ser  15559  clim2ser2  15560  isermulc2  15562  isercolllem3  15571  summolem3  15618  summolem2a  15619  fsumcl  15637  fsummulc2  15688  fsumrelem  15711  binom  15734  isumsplit  15744  risefacval2  15914  risefaccl  15919  risefallfac  15928  risefacp1  15933  binomfallfac  15945  binomrisefac  15946  bpoly3  15962  efcj  15996  ef4p  16019  tanval3  16040  efi4p  16043  sinadd  16070  cosadd  16071  tanadd  16073  addsin  16076  demoivreALT  16107  opoe  16271  pythagtriplem4  16728  pythagtriplem12  16735  pythagtriplem14  16737  pythagtriplem16  16739  gzaddcl  16846  cnaddablx  19778  cnaddabl  19779  cncrng  21323  cncrngOLD  21324  cnperf  24734  cnlmod  25065  cnstrcvs  25066  cncvs  25070  dvaddbr  25865  dvaddf  25870  dveflem  25908  plyaddcl  26150  plymulcl  26151  plysubcl  26152  coeaddlem  26179  dgrcolem1  26204  dgrcolem2  26205  quotlem  26233  quotcl2  26235  quotdgr  26236  sinperlem  26414  ptolemy  26430  tangtx  26439  sinkpi  26456  efif1olem2  26477  logrnaddcl  26508  logneg  26522  logimul  26548  cxpadd  26613  binom4  26785  atanf  26815  atanneg  26842  atancj  26845  efiatan  26847  atanlogaddlem  26848  atanlogadd  26849  atanlogsublem  26850  atanlogsub  26851  efiatan2  26852  2efiatan  26853  tanatan  26854  cosatan  26856  cosatanne0  26857  atantan  26858  atanbndlem  26860  atans2  26866  dvatan  26870  atantayl  26872  efrlim  26904  efrlimOLD  26905  dfef2  26906  gamcvg2lem  26994  ftalem7  27014  prmorcht  27113  bposlem9  27228  lgsquad2lem1  27320  2sqlem2  27354  cncph  30794  hhssnv  31239  hoadddir  31779  superpos  32329  knoppcnlem8  36533  cos2h  37650  tan2h  37651  ftc1anclem3  37734  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  facp2  42175  sumcubes  42345  fsumsermpt  45618  stirlinglem5  46115  stirlinglem7  46117  cnapbmcpd  47325  fmtnodvds  47574  opoeALTV  47713  mogoldbblem  47750