Theorem addcl 8248

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   + caddc 8126

This theorem was proved from axioms:  ax-addcl 8219

This theorem is referenced by:  adddir  8261  0cn  8262  addcli  8274  addcld  8289  muladd11  8402  peano2cn  8404  muladd11r  8425  add4  8430  cnegexlem3  8446  cnegex  8447  0cnALT  8459  negeu  8460  pncan  8475  2addsub  8483  addsubeq4  8484  nppcan2  8500  ppncan  8511  muladd  8653  mulsub  8670  recexap  8923  muleqadd  8938  conjmulap  8999  ofnegsub  9232  halfaddsubcl  9467  halfaddsub  9468  serf  10841  ser3add  10880  ser3sub  10881  ser0  10891  binom2  11009  binom3  11015  bernneq  11018  lswccatn0lsw  11292  shftlem  11494  shftval2  11504  shftval5  11507  2shfti  11509  crre  11535  crim  11536  cjadd  11562  addcj  11569  sqabsadd  11733  absreimsq  11745  absreim  11746  abstri  11782  addcn2  11988  climadd  12004  clim2ser  12015  clim2ser2  12016  isermulc2  12018  serf0  12030  sumrbdclem  12056  fsum3cvg  12057  summodclem3  12059  summodclem2a  12060  zsumdc  12063  fsum3  12066  fsum3cvg2  12073  fsum3ser  12076  fsumcl2lem  12077  fsumcl  12079  sumsnf  12088  fsummulc2  12127  binom  12163  isumshft  12169  isumsplit  12170  geolim2  12191  cvgratnnlemseq  12205  cvgratz  12211  ef0lem  12339  efcj  12352  ef4p  12373  efgt1p  12375  tanval3ap  12393  efi4p  12396  sinadd  12415  cosadd  12416  tanaddap  12418  addsin  12421  demoivreALT  12453  opoe  12574  pythagtriplem4  12959  pythagtriplem12  12966  gzaddcl  13068  cncrng  14704  addccncf  15452  dvaddxxbr  15553  dvaddxx  15555  dviaddf  15557  dveflem  15578  plyaddcl  15606  plymulcl  15607  plysubcl  15608  sinperlem  15660  ptolemy  15676  tangtx  15690  sinkpi  15699  binom4  15831  lgsquad2lem1  15941  2sqlem2  15975