Theorem addcl 8092

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970

This theorem was proved from axioms:  ax-addcl 8063

This theorem is referenced by:  adddir  8105  0cn  8106  addcli  8118  addcld  8134  muladd11  8247  peano2cn  8249  muladd11r  8270  add4  8275  cnegexlem3  8291  cnegex  8292  0cnALT  8304  negeu  8305  pncan  8320  2addsub  8328  addsubeq4  8329  nppcan2  8345  ppncan  8356  muladd  8498  mulsub  8515  recexap  8768  muleqadd  8783  conjmulap  8844  ofnegsub  9077  halfaddsubcl  9312  halfaddsub  9313  serf  10672  ser3add  10711  ser3sub  10712  ser0  10722  binom2  10840  binom3  10846  bernneq  10849  lswccatn0lsw  11112  shftlem  11293  shftval2  11303  shftval5  11306  2shfti  11308  crre  11334  crim  11335  cjadd  11361  addcj  11368  sqabsadd  11532  absreimsq  11544  absreim  11545  abstri  11581  addcn2  11787  climadd  11803  clim2ser  11814  clim2ser2  11815  isermulc2  11817  serf0  11829  sumrbdclem  11854  fsum3cvg  11855  summodclem3  11857  summodclem2a  11858  zsumdc  11861  fsum3  11864  fsum3cvg2  11871  fsum3ser  11874  fsumcl2lem  11875  fsumcl  11877  sumsnf  11886  fsummulc2  11925  binom  11961  isumshft  11967  isumsplit  11968  geolim2  11989  cvgratnnlemseq  12003  cvgratz  12009  ef0lem  12137  efcj  12150  ef4p  12171  efgt1p  12173  tanval3ap  12191  efi4p  12194  sinadd  12213  cosadd  12214  tanaddap  12216  addsin  12219  demoivreALT  12251  opoe  12372  pythagtriplem4  12757  pythagtriplem12  12764  gzaddcl  12866  cncrng  14498  addccncf  15239  dvaddxxbr  15340  dvaddxx  15342  dviaddf  15344  dveflem  15365  plyaddcl  15393  plymulcl  15394  plysubcl  15395  sinperlem  15447  ptolemy  15463  tangtx  15477  sinkpi  15486  binom4  15618  lgsquad2lem1  15725  2sqlem2  15759