Theorem addcl 8257

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   + caddc 8135

This theorem was proved from axioms:  ax-addcl 8228

This theorem is referenced by:  adddir  8270  0cn  8271  addcli  8283  addcld  8298  muladd11  8411  peano2cn  8413  muladd11r  8434  add4  8439  cnegexlem3  8455  cnegex  8456  0cnALT  8468  negeu  8469  pncan  8484  2addsub  8492  addsubeq4  8493  nppcan2  8509  ppncan  8520  muladd  8662  mulsub  8679  recexap  8932  muleqadd  8947  conjmulap  9008  ofnegsub  9241  halfaddsubcl  9476  halfaddsub  9477  serf  10852  ser3add  10891  ser3sub  10892  ser0  10902  binom2  11020  binom3  11026  bernneq  11030  lswccatn0lsw  11307  shftlem  11509  shftval2  11519  shftval5  11522  2shfti  11524  crre  11550  crim  11551  cjadd  11577  addcj  11584  sqabsadd  11748  absreimsq  11760  absreim  11761  abstri  11797  addcn2  12003  climadd  12019  clim2ser  12030  clim2ser2  12031  isermulc2  12033  serf0  12045  sumrbdclem  12071  fsum3cvg  12072  summodclem3  12074  summodclem2a  12075  zsumdc  12078  fsum3  12081  fsum3cvg2  12088  fsum3ser  12091  fsumcl2lem  12092  fsumcl  12094  sumsnf  12103  fsummulc2  12142  binom  12178  isumshft  12184  isumsplit  12185  geolim2  12206  cvgratnnlemseq  12220  cvgratz  12226  ef0lem  12354  efcj  12367  ef4p  12388  efgt1p  12390  tanval3ap  12408  efi4p  12411  sinadd  12430  cosadd  12431  tanaddap  12433  addsin  12436  demoivreALT  12468  opoe  12589  pythagtriplem4  12974  pythagtriplem12  12981  gzaddcl  13083  cncrng  14766  addccncf  15514  dvaddxxbr  15615  dvaddxx  15617  dviaddf  15619  dveflem  15640  plyaddcl  15668  plymulcl  15669  plysubcl  15670  sinperlem  15722  ptolemy  15738  tangtx  15752  sinkpi  15761  binom4  15893  lgsquad2lem1  16003  2sqlem2  16037