Theorem addcl 8147

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6013   CCcc 8020   + caddc 8025

This theorem was proved from axioms:  ax-addcl 8118

This theorem is referenced by:  adddir  8160  0cn  8161  addcli  8173  addcld  8189  muladd11  8302  peano2cn  8304  muladd11r  8325  add4  8330  cnegexlem3  8346  cnegex  8347  0cnALT  8359  negeu  8360  pncan  8375  2addsub  8383  addsubeq4  8384  nppcan2  8400  ppncan  8411  muladd  8553  mulsub  8570  recexap  8823  muleqadd  8838  conjmulap  8899  ofnegsub  9132  halfaddsubcl  9367  halfaddsub  9368  serf  10735  ser3add  10774  ser3sub  10775  ser0  10785  binom2  10903  binom3  10909  bernneq  10912  lswccatn0lsw  11178  shftlem  11367  shftval2  11377  shftval5  11380  2shfti  11382  crre  11408  crim  11409  cjadd  11435  addcj  11442  sqabsadd  11606  absreimsq  11618  absreim  11619  abstri  11655  addcn2  11861  climadd  11877  clim2ser  11888  clim2ser2  11889  isermulc2  11891  serf0  11903  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsum3  11938  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumcl  11951  sumsnf  11960  fsummulc2  11999  binom  12035  isumshft  12041  isumsplit  12042  geolim2  12063  cvgratnnlemseq  12077  cvgratz  12083  ef0lem  12211  efcj  12224  ef4p  12245  efgt1p  12247  tanval3ap  12265  efi4p  12268  sinadd  12287  cosadd  12288  tanaddap  12290  addsin  12293  demoivreALT  12325  opoe  12446  pythagtriplem4  12831  pythagtriplem12  12838  gzaddcl  12940  cncrng  14573  addccncf  15314  dvaddxxbr  15415  dvaddxx  15417  dviaddf  15419  dveflem  15440  plyaddcl  15468  plymulcl  15469  plysubcl  15470  sinperlem  15522  ptolemy  15538  tangtx  15552  sinkpi  15561  binom4  15693  lgsquad2lem1  15800  2sqlem2  15834