Theorem addcl 7967

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2160  (class class class)co 5897   CCcc 7840   + caddc 7845

This theorem was proved from axioms:  ax-addcl 7938

This theorem is referenced by:  adddir  7979  0cn  7980  addcli  7992  addcld  8008  muladd11  8121  peano2cn  8123  muladd11r  8144  add4  8149  cnegexlem3  8165  cnegex  8166  0cnALT  8178  negeu  8179  pncan  8194  2addsub  8202  addsubeq4  8203  nppcan2  8219  ppncan  8230  muladd  8372  mulsub  8389  recexap  8641  muleqadd  8656  conjmulap  8717  halfaddsubcl  9183  halfaddsub  9184  serf  10507  ser3add  10538  ser3sub  10539  ser0  10548  binom2  10666  binom3  10672  bernneq  10675  shftlem  10860  shftval2  10870  shftval5  10873  2shfti  10875  crre  10901  crim  10902  cjadd  10928  addcj  10935  sqabsadd  11099  absreimsq  11111  absreim  11112  abstri  11148  addcn2  11353  climadd  11369  clim2ser  11380  clim2ser2  11381  isermulc2  11383  serf0  11395  sumrbdclem  11420  fsum3cvg  11421  summodclem3  11423  summodclem2a  11424  zsumdc  11427  fsum3  11430  fsum3cvg2  11437  fsum3ser  11440  fsumcl2lem  11441  fsumcl  11443  sumsnf  11452  fsummulc2  11491  binom  11527  isumshft  11533  isumsplit  11534  geolim2  11555  cvgratnnlemseq  11569  cvgratz  11575  ef0lem  11703  efcj  11716  ef4p  11737  efgt1p  11739  tanval3ap  11757  efi4p  11760  sinadd  11779  cosadd  11780  tanaddap  11782  addsin  11785  demoivreALT  11816  opoe  11935  pythagtriplem4  12303  pythagtriplem12  12310  gzaddcl  12412  cncrng  13889  addccncf  14563  dvaddxxbr  14642  dvaddxx  14644  dviaddf  14646  dveflem  14664  sinperlem  14706  ptolemy  14722  tangtx  14736  sinkpi  14745  binom4  14874  2sqlem2  14940