Theorem addcl 8162

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   + caddc 8040

This theorem was proved from axioms:  ax-addcl 8133

This theorem is referenced by:  adddir  8175  0cn  8176  addcli  8188  addcld  8204  muladd11  8317  peano2cn  8319  muladd11r  8340  add4  8345  cnegexlem3  8361  cnegex  8362  0cnALT  8374  negeu  8375  pncan  8390  2addsub  8398  addsubeq4  8399  nppcan2  8415  ppncan  8426  muladd  8568  mulsub  8585  recexap  8838  muleqadd  8853  conjmulap  8914  ofnegsub  9147  halfaddsubcl  9382  halfaddsub  9383  serf  10751  ser3add  10790  ser3sub  10791  ser0  10801  binom2  10919  binom3  10925  bernneq  10928  lswccatn0lsw  11197  shftlem  11399  shftval2  11409  shftval5  11412  2shfti  11414  crre  11440  crim  11441  cjadd  11467  addcj  11474  sqabsadd  11638  absreimsq  11650  absreim  11651  abstri  11687  addcn2  11893  climadd  11909  clim2ser  11920  clim2ser2  11921  isermulc2  11923  serf0  11935  sumrbdclem  11961  fsum3cvg  11962  summodclem3  11964  summodclem2a  11965  zsumdc  11968  fsum3  11971  fsum3cvg2  11978  fsum3ser  11981  fsumcl2lem  11982  fsumcl  11984  sumsnf  11993  fsummulc2  12032  binom  12068  isumshft  12074  isumsplit  12075  geolim2  12096  cvgratnnlemseq  12110  cvgratz  12116  ef0lem  12244  efcj  12257  ef4p  12278  efgt1p  12280  tanval3ap  12298  efi4p  12301  sinadd  12320  cosadd  12321  tanaddap  12323  addsin  12326  demoivreALT  12358  opoe  12479  pythagtriplem4  12864  pythagtriplem12  12871  gzaddcl  12973  cncrng  14607  addccncf  15353  dvaddxxbr  15454  dvaddxx  15456  dviaddf  15458  dveflem  15479  plyaddcl  15507  plymulcl  15508  plysubcl  15509  sinperlem  15561  ptolemy  15577  tangtx  15591  sinkpi  15600  binom4  15732  lgsquad2lem1  15839  2sqlem2  15873