Theorem addcl 7938

Description: Alias for ax-addcl 7909, for naming consistency with addcli 7963. Use this theorem instead of ax-addcl 7909 or axaddcl 7865. (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 7909	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148  (class class class)co 5877   CCcc 7811   + caddc 7816

This theorem was proved from axioms:  ax-addcl 7909

This theorem is referenced by:  adddir  7950  0cn  7951  addcli  7963  addcld  7979  muladd11  8092  peano2cn  8094  muladd11r  8115  add4  8120  cnegexlem3  8136  cnegex  8137  0cnALT  8149  negeu  8150  pncan  8165  2addsub  8173  addsubeq4  8174  nppcan2  8190  ppncan  8201  muladd  8343  mulsub  8360  recexap  8612  muleqadd  8627  conjmulap  8688  halfaddsubcl  9154  halfaddsub  9155  serf  10476  ser3add  10507  ser3sub  10508  ser0  10516  binom2  10634  binom3  10640  bernneq  10643  shftlem  10827  shftval2  10837  shftval5  10840  2shfti  10842  crre  10868  crim  10869  cjadd  10895  addcj  10902  sqabsadd  11066  absreimsq  11078  absreim  11079  abstri  11115  addcn2  11320  climadd  11336  clim2ser  11347  clim2ser2  11348  isermulc2  11350  serf0  11362  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsum3  11397  fsum3cvg2  11404  fsum3ser  11407  fsumcl2lem  11408  fsumcl  11410  sumsnf  11419  fsummulc2  11458  binom  11494  isumshft  11500  isumsplit  11501  geolim2  11522  cvgratnnlemseq  11536  cvgratz  11542  ef0lem  11670  efcj  11683  ef4p  11704  efgt1p  11706  tanval3ap  11724  efi4p  11727  sinadd  11746  cosadd  11747  tanaddap  11749  addsin  11752  demoivreALT  11783  opoe  11902  pythagtriplem4  12270  pythagtriplem12  12277  gzaddcl  12377  cncrng  13502  addccncf  14125  dvaddxxbr  14204  dvaddxx  14206  dviaddf  14208  dveflem  14226  sinperlem  14268  ptolemy  14284  tangtx  14298  sinkpi  14307  binom4  14436  2sqlem2  14501