Theorem addcl 8304

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182

This proof depends on axioms:  ax-addcl 8275

This theorem is used by:  adddir  8317  0cn  8318  addcli  8330  addcld  8345  muladd11  8459  peano2cn  8461  muladd11r  8482  add4  8487  cnegexlem3  8503  cnegex  8504  0cnALT  8516  negeu  8517  pncan  8532  2addsub  8540  addsubeq4  8541  nppcan2  8557  ppncan  8568  muladd  8711  mulsub  8728  recexap  8982  muleqadd  8999  conjmulap  9060  ofnegsub  9293  halfaddsubcl  9540  halfaddsub  9541  serf  10922  ser3add  10961  ser3sub  10962  ser0  10972  binom2  11090  binom3  11096  bernneq  11100  lswccatn0lsw  11381  shftlem  11583  shftval2  11593  shftval5  11596  2shfti  11598  crre  11624  crim  11625  cjadd  11651  addcj  11658  sqabsadd  11823  absreimsq  11835  absreim  11836  abstri  11872  addcn2  12078  climadd  12094  clim2ser  12105  clim2ser2  12106  isermulc2  12108  serf0  12120  sumrbdclem  12146  fsum3cvg  12147  summodclem3  12149  summodclem2a  12150  zsumdc  12153  fsum3  12156  fsum3cvg2  12163  fsum3ser  12166  fsumcl2lem  12167  fsumcl  12169  sumsnf  12178  fsummulc2  12217  binom  12253  isumshft  12259  isumsplit  12260  geolim2  12281  cvgratnnlemseq  12295  cvgratz  12301  ef0lem  12429  efcj  12442  ef4p  12463  efgt1p  12465  tanval3ap  12483  efi4p  12486  sinadd  12505  cosadd  12506  tanaddap  12508  addsin  12511  demoivreALT  12543  opoe  12664  pythagtriplem4  13049  pythagtriplem12  13056  gzaddcl  13158  cncrng  14908  addccncf  15703  dvaddxxbr  15804  dvaddxx  15806  dviaddf  15808  dveflem  15829  plyaddcl  15857  plymulcl  15858  plysubcl  15859  sinperlem  15912  ptolemy  15928  tangtx  15942  sinkpi  15951  binom4  16087  lgsquad2lem1  16212  2sqlem2  16246