Theorem addcl 8311

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

Assertion

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

Proof of Theorem addcl

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

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

This proof depends on axioms:  ax-addcl 8282

This theorem is used by:  adddir  8324  0cn  8325  addcli  8337  addcld  8352  muladd11  8467  peano2cn  8469  muladd11r  8490  add4  8495  cnegexlem3  8511  cnegex  8512  0cnALT  8524  negeu  8525  pncan  8540  2addsub  8548  addsubeq4  8549  nppcan2  8565  ppncan  8576  muladd  8719  mulsub  8736  recexap  8990  muleqadd  9007  conjmulap  9068  ofnegsub  9302  halfaddsubcl  9550  halfaddsub  9551  serf  10942  ser3add  10981  ser3sub  10982  ser0  10992  binom2  11110  binom3  11116  bernneq  11120  lswccatn0lsw  11402  shftlem  11604  shftval2  11614  shftval5  11617  2shfti  11619  crre  11645  crim  11646  cjadd  11672  addcj  11679  sqabsadd  11844  absreimsq  11856  absreim  11857  abstri  11894  addcn2  12102  climadd  12118  clim2ser  12129  clim2ser2  12130  isermulc2  12132  serf0  12144  sumrbdclem  12170  fsum3cvg  12171  summodclem3  12173  summodclem2a  12174  zsumdc  12177  fsum3  12180  fsum3cvg2  12187  fsum3ser  12190  fsumcl2lem  12191  fsumcl  12193  sumsnf  12202  fsummulc2  12241  binom  12277  isumshft  12283  isumsplit  12284  geolim2  12305  cvgratnnlemseq  12319  cvgratz  12325  ef0lem  12453  efcj  12466  ef4p  12487  efgt1p  12489  tanval3ap  12507  efi4p  12510  sinadd  12529  cosadd  12530  tanaddap  12532  addsin  12535  demoivreALT  12567  opoe  12688  pythagtriplem4  13077  pythagtriplem12  13084  gzaddcl  13186  cncrng  15016  addccncf  15838  dvaddxxbr  15939  dvaddxx  15941  dviaddf  15943  dveflem  15964  plyaddcl  15992  plymulcl  15993  plysubcl  15994  sinperlem  16047  ptolemy  16063  tangtx  16077  sinkpi  16086  binom4  16231  prmorcht  16294  bposlem9  16331  lgsquad2lem1  16417  2sqlem2  16451