Theorem addcl 8004

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   + caddc 7882

This theorem was proved from axioms:  ax-addcl 7975

This theorem is referenced by:  adddir  8017  0cn  8018  addcli  8030  addcld  8046  muladd11  8159  peano2cn  8161  muladd11r  8182  add4  8187  cnegexlem3  8203  cnegex  8204  0cnALT  8216  negeu  8217  pncan  8232  2addsub  8240  addsubeq4  8241  nppcan2  8257  ppncan  8268  muladd  8410  mulsub  8427  recexap  8680  muleqadd  8695  conjmulap  8756  ofnegsub  8989  halfaddsubcl  9224  halfaddsub  9225  serf  10575  ser3add  10614  ser3sub  10615  ser0  10625  binom2  10743  binom3  10749  bernneq  10752  shftlem  10981  shftval2  10991  shftval5  10994  2shfti  10996  crre  11022  crim  11023  cjadd  11049  addcj  11056  sqabsadd  11220  absreimsq  11232  absreim  11233  abstri  11269  addcn2  11475  climadd  11491  clim2ser  11502  clim2ser2  11503  isermulc2  11505  serf0  11517  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsum3  11552  fsum3cvg2  11559  fsum3ser  11562  fsumcl2lem  11563  fsumcl  11565  sumsnf  11574  fsummulc2  11613  binom  11649  isumshft  11655  isumsplit  11656  geolim2  11677  cvgratnnlemseq  11691  cvgratz  11697  ef0lem  11825  efcj  11838  ef4p  11859  efgt1p  11861  tanval3ap  11879  efi4p  11882  sinadd  11901  cosadd  11902  tanaddap  11904  addsin  11907  demoivreALT  11939  opoe  12060  pythagtriplem4  12437  pythagtriplem12  12444  gzaddcl  12546  cncrng  14125  addccncf  14836  dvaddxxbr  14937  dvaddxx  14939  dviaddf  14941  dveflem  14962  plyaddcl  14990  plymulcl  14991  plysubcl  14992  sinperlem  15044  ptolemy  15060  tangtx  15074  sinkpi  15083  binom4  15215  lgsquad2lem1  15322  2sqlem2  15356