Theorem addcl 7869

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2135  (class class class)co 5836  ℂcc 7742   + caddc 7747

This theorem was proved from axioms:  ax-addcl 7840

This theorem is referenced by:  adddir  7881  0cn  7882  addcli  7894  addcld  7909  muladd11  8022  peano2cn  8024  muladd11r  8045  add4  8050  cnegexlem3  8066  cnegex  8067  0cnALT  8079  negeu  8080  pncan  8095  2addsub  8103  addsubeq4  8104  nppcan2  8120  ppncan  8131  muladd  8273  mulsub  8290  recexap  8541  muleqadd  8556  conjmulap  8616  halfaddsubcl  9081  halfaddsub  9082  serf  10399  ser3add  10430  ser3sub  10431  ser0  10439  binom2  10555  binom3  10561  bernneq  10564  shftlem  10744  shftval2  10754  shftval5  10757  2shfti  10759  crre  10785  crim  10786  cjadd  10812  addcj  10819  sqabsadd  10983  absreimsq  10995  absreim  10996  abstri  11032  addcn2  11237  climadd  11253  clim2ser  11264  clim2ser2  11265  isermulc2  11267  serf0  11279  sumrbdclem  11304  fsum3cvg  11305  summodclem3  11307  summodclem2a  11308  zsumdc  11311  fsum3  11314  fsum3cvg2  11321  fsum3ser  11324  fsumcl2lem  11325  fsumcl  11327  sumsnf  11336  fsummulc2  11375  binom  11411  isumshft  11417  isumsplit  11418  geolim2  11439  cvgratnnlemseq  11453  cvgratz  11459  ef0lem  11587  efcj  11600  ef4p  11621  efgt1p  11623  tanval3ap  11641  efi4p  11644  sinadd  11663  cosadd  11664  tanaddap  11666  addsin  11669  demoivreALT  11700  opoe  11817  pythagtriplem4  12177  pythagtriplem12  12184  addccncf  13127  dvaddxxbr  13206  dvaddxx  13208  dviaddf  13210  dveflem  13228  sinperlem  13270  ptolemy  13286  tangtx  13300  sinkpi  13309  binom4  13438