Theorem addcl 8298

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176

This theorem was proved from axioms:  ax-addcl 8269

This theorem is referenced by:  adddir  8311  0cn  8312  addcli  8324  addcld  8339  muladd11  8453  peano2cn  8455  muladd11r  8476  add4  8481  cnegexlem3  8497  cnegex  8498  0cnALT  8510  negeu  8511  pncan  8526  2addsub  8534  addsubeq4  8535  nppcan2  8551  ppncan  8562  muladd  8705  mulsub  8722  recexap  8975  muleqadd  8992  conjmulap  9053  ofnegsub  9286  halfaddsubcl  9521  halfaddsub  9522  serf  10903  ser3add  10942  ser3sub  10943  ser0  10953  binom2  11071  binom3  11077  bernneq  11081  lswccatn0lsw  11362  shftlem  11564  shftval2  11574  shftval5  11577  2shfti  11579  crre  11605  crim  11606  cjadd  11632  addcj  11639  sqabsadd  11804  absreimsq  11816  absreim  11817  abstri  11853  addcn2  12059  climadd  12075  clim2ser  12086  clim2ser2  12087  isermulc2  12089  serf0  12101  sumrbdclem  12127  fsum3cvg  12128  summodclem3  12130  summodclem2a  12131  zsumdc  12134  fsum3  12137  fsum3cvg2  12144  fsum3ser  12147  fsumcl2lem  12148  fsumcl  12150  sumsnf  12159  fsummulc2  12198  binom  12234  isumshft  12240  isumsplit  12241  geolim2  12262  cvgratnnlemseq  12276  cvgratz  12282  ef0lem  12410  efcj  12423  ef4p  12444  efgt1p  12446  tanval3ap  12464  efi4p  12467  sinadd  12486  cosadd  12487  tanaddap  12489  addsin  12492  demoivreALT  12524  opoe  12645  pythagtriplem4  13030  pythagtriplem12  13037  gzaddcl  13139  cncrng  14889  addccncf  15684  dvaddxxbr  15785  dvaddxx  15787  dviaddf  15789  dveflem  15810  plyaddcl  15838  plymulcl  15839  plysubcl  15840  sinperlem  15892  ptolemy  15908  tangtx  15922  sinkpi  15931  binom4  16064  lgsquad2lem1  16183  2sqlem2  16217