Theorem addcl 8057

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   + caddc 7935

This theorem was proved from axioms:  ax-addcl 8028

This theorem is referenced by:  adddir  8070  0cn  8071  addcli  8083  addcld  8099  muladd11  8212  peano2cn  8214  muladd11r  8235  add4  8240  cnegexlem3  8256  cnegex  8257  0cnALT  8269  negeu  8270  pncan  8285  2addsub  8293  addsubeq4  8294  nppcan2  8310  ppncan  8321  muladd  8463  mulsub  8480  recexap  8733  muleqadd  8748  conjmulap  8809  ofnegsub  9042  halfaddsubcl  9277  halfaddsub  9278  serf  10635  ser3add  10674  ser3sub  10675  ser0  10685  binom2  10803  binom3  10809  bernneq  10812  lswccatn0lsw  11075  shftlem  11171  shftval2  11181  shftval5  11184  2shfti  11186  crre  11212  crim  11213  cjadd  11239  addcj  11246  sqabsadd  11410  absreimsq  11422  absreim  11423  abstri  11459  addcn2  11665  climadd  11681  clim2ser  11692  clim2ser2  11693  isermulc2  11695  serf0  11707  sumrbdclem  11732  fsum3cvg  11733  summodclem3  11735  summodclem2a  11736  zsumdc  11739  fsum3  11742  fsum3cvg2  11749  fsum3ser  11752  fsumcl2lem  11753  fsumcl  11755  sumsnf  11764  fsummulc2  11803  binom  11839  isumshft  11845  isumsplit  11846  geolim2  11867  cvgratnnlemseq  11881  cvgratz  11887  ef0lem  12015  efcj  12028  ef4p  12049  efgt1p  12051  tanval3ap  12069  efi4p  12072  sinadd  12091  cosadd  12092  tanaddap  12094  addsin  12097  demoivreALT  12129  opoe  12250  pythagtriplem4  12635  pythagtriplem12  12642  gzaddcl  12744  cncrng  14375  addccncf  15116  dvaddxxbr  15217  dvaddxx  15219  dviaddf  15221  dveflem  15242  plyaddcl  15270  plymulcl  15271  plysubcl  15272  sinperlem  15324  ptolemy  15340  tangtx  15354  sinkpi  15363  binom4  15495  lgsquad2lem1  15602  2sqlem2  15636