Theorem addcl 10608

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529

This theorem was proved from axioms:  ax-addcl 10586

This theorem is referenced by:  adddir  10621  0cn  10622  addcli  10636  addcld  10649  muladd11  10799  peano2cn  10801  muladd11r  10842  add4  10849  0cnALT2  10864  negeu  10865  pncan  10881  2addsub  10889  addsubeq4  10890  nppcan2  10906  pnpcan  10914  ppncan  10917  muladd  11061  mulsub  11072  recex  11261  muleqadd  11273  conjmul  11346  halfaddsubcl  11857  halfaddsub  11858  serf  13394  seradd  13408  sersub  13409  binom3  13581  bernneq  13586  lswccatn0lsw  13936  revccat  14119  2cshwcshw  14178  shftlem  14419  shftval2  14426  shftval5  14429  2shfti  14431  crre  14465  crim  14466  cjadd  14492  addcj  14499  sqabsadd  14634  absreimsq  14644  absreim  14645  abstri  14682  sqreulem  14711  sqreu  14712  addcn2  14942  o1add  14962  climadd  14980  clim2ser  15003  clim2ser2  15004  isermulc2  15006  isercolllem3  15015  summolem3  15063  summolem2a  15064  fsumcl  15082  fsummulc2  15131  fsumrelem  15154  binom  15177  isumsplit  15187  risefacval2  15356  risefaccl  15361  risefallfac  15370  risefacp1  15375  binomfallfac  15387  binomrisefac  15388  bpoly3  15404  efcj  15437  ef4p  15458  tanval3  15479  efi4p  15482  sinadd  15509  cosadd  15510  tanadd  15512  addsin  15515  demoivreALT  15546  opoe  15704  pythagtriplem4  16146  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  gzaddcl  16263  cnaddablx  18981  cnaddabl  18982  cncrng  20112  cnperf  23425  cnlmod  23745  cnstrcvs  23746  cncvs  23750  dvaddbr  24541  dvaddf  24545  dveflem  24582  plyaddcl  24817  plymulcl  24818  plysubcl  24819  coeaddlem  24846  dgrcolem1  24870  dgrcolem2  24871  quotlem  24896  quotcl2  24898  quotdgr  24899  sinperlem  25073  ptolemy  25089  tangtx  25098  sinkpi  25114  efif1olem2  25135  logrnaddcl  25166  logneg  25179  logimul  25205  cxpadd  25270  binom4  25436  atanf  25466  atanneg  25493  atancj  25496  efiatan  25498  atanlogaddlem  25499  atanlogadd  25500  atanlogsublem  25501  atanlogsub  25502  efiatan2  25503  2efiatan  25504  tanatan  25505  cosatan  25507  cosatanne0  25508  atantan  25509  atanbndlem  25511  atans2  25517  dvatan  25521  atantayl  25523  efrlim  25555  dfef2  25556  gamcvg2lem  25644  ftalem7  25664  prmorcht  25763  bposlem9  25876  lgsquad2lem1  25968  2sqlem2  26002  cncph  28602  hhssnv  29047  hoadddir  29587  superpos  30137  knoppcnlem8  33952  cos2h  35048  tan2h  35049  ftc1anclem3  35132  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  facp2  39347  fac2xp3  39385  fsumsermpt  42221  stirlinglem5  42720  stirlinglem7  42722  cnapbmcpd  43852  fmtnodvds  44061  opoeALTV  44201  mogoldbblem  44238