Theorem addcl 8268

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146

This theorem was proved from axioms:  ax-addcl 8239

This theorem is referenced by:  adddir  8281  0cn  8282  addcli  8294  addcld  8309  muladd11  8423  peano2cn  8425  muladd11r  8446  add4  8451  cnegexlem3  8467  cnegex  8468  0cnALT  8480  negeu  8481  pncan  8496  2addsub  8504  addsubeq4  8505  nppcan2  8521  ppncan  8532  muladd  8675  mulsub  8692  recexap  8945  muleqadd  8962  conjmulap  9023  ofnegsub  9256  halfaddsubcl  9491  halfaddsub  9492  serf  10872  ser3add  10911  ser3sub  10912  ser0  10922  binom2  11040  binom3  11046  bernneq  11050  lswccatn0lsw  11327  shftlem  11529  shftval2  11539  shftval5  11542  2shfti  11544  crre  11570  crim  11571  cjadd  11597  addcj  11604  sqabsadd  11768  absreimsq  11780  absreim  11781  abstri  11817  addcn2  12023  climadd  12039  clim2ser  12050  clim2ser2  12051  isermulc2  12053  serf0  12065  sumrbdclem  12091  fsum3cvg  12092  summodclem3  12094  summodclem2a  12095  zsumdc  12098  fsum3  12101  fsum3cvg2  12108  fsum3ser  12111  fsumcl2lem  12112  fsumcl  12114  sumsnf  12123  fsummulc2  12162  binom  12198  isumshft  12204  isumsplit  12205  geolim2  12226  cvgratnnlemseq  12240  cvgratz  12246  ef0lem  12374  efcj  12387  ef4p  12408  efgt1p  12410  tanval3ap  12428  efi4p  12431  sinadd  12450  cosadd  12451  tanaddap  12453  addsin  12456  demoivreALT  12488  opoe  12609  pythagtriplem4  12994  pythagtriplem12  13001  gzaddcl  13103  cncrng  14846  addccncf  15594  dvaddxxbr  15695  dvaddxx  15697  dviaddf  15699  dveflem  15720  plyaddcl  15748  plymulcl  15749  plysubcl  15750  sinperlem  15802  ptolemy  15818  tangtx  15832  sinkpi  15841  binom4  15973  lgsquad2lem1  16083  2sqlem2  16117