Theorem addcl 8070

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

Assertion

Ref	Expression
addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Proof of Theorem addcl

Step	Hyp	Ref	Expression
1		ax-addcl 8041	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2177  (class class class)co 5957   CCcc 7943   + caddc 7948

This theorem was proved from axioms:  ax-addcl 8041

This theorem is referenced by:  adddir  8083  0cn  8084  addcli  8096  addcld  8112  muladd11  8225  peano2cn  8227  muladd11r  8248  add4  8253  cnegexlem3  8269  cnegex  8270  0cnALT  8282  negeu  8283  pncan  8298  2addsub  8306  addsubeq4  8307  nppcan2  8323  ppncan  8334  muladd  8476  mulsub  8493  recexap  8746  muleqadd  8761  conjmulap  8822  ofnegsub  9055  halfaddsubcl  9290  halfaddsub  9291  serf  10650  ser3add  10689  ser3sub  10690  ser0  10700  binom2  10818  binom3  10824  bernneq  10827  lswccatn0lsw  11090  shftlem  11202  shftval2  11212  shftval5  11215  2shfti  11217  crre  11243  crim  11244  cjadd  11270  addcj  11277  sqabsadd  11441  absreimsq  11453  absreim  11454  abstri  11490  addcn2  11696  climadd  11712  clim2ser  11723  clim2ser2  11724  isermulc2  11726  serf0  11738  sumrbdclem  11763  fsum3cvg  11764  summodclem3  11766  summodclem2a  11767  zsumdc  11770  fsum3  11773  fsum3cvg2  11780  fsum3ser  11783  fsumcl2lem  11784  fsumcl  11786  sumsnf  11795  fsummulc2  11834  binom  11870  isumshft  11876  isumsplit  11877  geolim2  11898  cvgratnnlemseq  11912  cvgratz  11918  ef0lem  12046  efcj  12059  ef4p  12080  efgt1p  12082  tanval3ap  12100  efi4p  12103  sinadd  12122  cosadd  12123  tanaddap  12125  addsin  12128  demoivreALT  12160  opoe  12281  pythagtriplem4  12666  pythagtriplem12  12673  gzaddcl  12775  cncrng  14406  addccncf  15147  dvaddxxbr  15248  dvaddxx  15250  dviaddf  15252  dveflem  15273  plyaddcl  15301  plymulcl  15302  plysubcl  15303  sinperlem  15355  ptolemy  15371  tangtx  15385  sinkpi  15394  binom4  15526  lgsquad2lem1  15633  2sqlem2  15667