Theorem addcl 7935

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   + caddc 7813

This theorem was proved from axioms:  ax-addcl 7906

This theorem is referenced by:  adddir  7947  0cn  7948  addcli  7960  addcld  7975  muladd11  8088  peano2cn  8090  muladd11r  8111  add4  8116  cnegexlem3  8132  cnegex  8133  0cnALT  8145  negeu  8146  pncan  8161  2addsub  8169  addsubeq4  8170  nppcan2  8186  ppncan  8197  muladd  8339  mulsub  8356  recexap  8608  muleqadd  8623  conjmulap  8684  halfaddsubcl  9150  halfaddsub  9151  serf  10471  ser3add  10502  ser3sub  10503  ser0  10511  binom2  10628  binom3  10634  bernneq  10637  shftlem  10820  shftval2  10830  shftval5  10833  2shfti  10835  crre  10861  crim  10862  cjadd  10888  addcj  10895  sqabsadd  11059  absreimsq  11071  absreim  11072  abstri  11108  addcn2  11313  climadd  11329  clim2ser  11340  clim2ser2  11341  isermulc2  11343  serf0  11355  sumrbdclem  11380  fsum3cvg  11381  summodclem3  11383  summodclem2a  11384  zsumdc  11387  fsum3  11390  fsum3cvg2  11397  fsum3ser  11400  fsumcl2lem  11401  fsumcl  11403  sumsnf  11412  fsummulc2  11451  binom  11487  isumshft  11493  isumsplit  11494  geolim2  11515  cvgratnnlemseq  11529  cvgratz  11535  ef0lem  11663  efcj  11676  ef4p  11697  efgt1p  11699  tanval3ap  11717  efi4p  11720  sinadd  11739  cosadd  11740  tanaddap  11742  addsin  11745  demoivreALT  11776  opoe  11894  pythagtriplem4  12262  pythagtriplem12  12269  gzaddcl  12369  cncrng  13354  addccncf  13979  dvaddxxbr  14058  dvaddxx  14060  dviaddf  14062  dveflem  14080  sinperlem  14122  ptolemy  14138  tangtx  14152  sinkpi  14161  binom4  14290  2sqlem2  14344