Theorem addcl 7931

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5870  ℂcc 7804   + caddc 7809

This theorem was proved from axioms:  ax-addcl 7902

This theorem is referenced by:  adddir  7943  0cn  7944  addcli  7956  addcld  7971  muladd11  8084  peano2cn  8086  muladd11r  8107  add4  8112  cnegexlem3  8128  cnegex  8129  0cnALT  8141  negeu  8142  pncan  8157  2addsub  8165  addsubeq4  8166  nppcan2  8182  ppncan  8193  muladd  8335  mulsub  8352  recexap  8604  muleqadd  8619  conjmulap  8680  halfaddsubcl  9146  halfaddsub  9147  serf  10467  ser3add  10498  ser3sub  10499  ser0  10507  binom2  10624  binom3  10630  bernneq  10633  shftlem  10816  shftval2  10826  shftval5  10829  2shfti  10831  crre  10857  crim  10858  cjadd  10884  addcj  10891  sqabsadd  11055  absreimsq  11067  absreim  11068  abstri  11104  addcn2  11309  climadd  11325  clim2ser  11336  clim2ser2  11337  isermulc2  11339  serf0  11351  sumrbdclem  11376  fsum3cvg  11377  summodclem3  11379  summodclem2a  11380  zsumdc  11383  fsum3  11386  fsum3cvg2  11393  fsum3ser  11396  fsumcl2lem  11397  fsumcl  11399  sumsnf  11408  fsummulc2  11447  binom  11483  isumshft  11489  isumsplit  11490  geolim2  11511  cvgratnnlemseq  11525  cvgratz  11531  ef0lem  11659  efcj  11672  ef4p  11693  efgt1p  11695  tanval3ap  11713  efi4p  11716  sinadd  11735  cosadd  11736  tanaddap  11738  addsin  11741  demoivreALT  11772  opoe  11890  pythagtriplem4  12258  pythagtriplem12  12265  gzaddcl  12365  cncrng  13268  addccncf  13868  dvaddxxbr  13947  dvaddxx  13949  dviaddf  13951  dveflem  13969  sinperlem  14011  ptolemy  14027  tangtx  14041  sinkpi  14050  binom4  14179  2sqlem2  14233