Theorem addcl 8252

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130

This theorem was proved from axioms:  ax-addcl 8223

This theorem is referenced by:  adddir  8265  0cn  8266  addcli  8278  addcld  8293  muladd11  8406  peano2cn  8408  muladd11r  8429  add4  8434  cnegexlem3  8450  cnegex  8451  0cnALT  8463  negeu  8464  pncan  8479  2addsub  8487  addsubeq4  8488  nppcan2  8504  ppncan  8515  muladd  8657  mulsub  8674  recexap  8927  muleqadd  8942  conjmulap  9003  ofnegsub  9236  halfaddsubcl  9471  halfaddsub  9472  serf  10845  ser3add  10884  ser3sub  10885  ser0  10895  binom2  11013  binom3  11019  bernneq  11022  lswccatn0lsw  11299  shftlem  11501  shftval2  11511  shftval5  11514  2shfti  11516  crre  11542  crim  11543  cjadd  11569  addcj  11576  sqabsadd  11740  absreimsq  11752  absreim  11753  abstri  11789  addcn2  11995  climadd  12011  clim2ser  12022  clim2ser2  12023  isermulc2  12025  serf0  12037  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsum3  12073  fsum3cvg2  12080  fsum3ser  12083  fsumcl2lem  12084  fsumcl  12086  sumsnf  12095  fsummulc2  12134  binom  12170  isumshft  12176  isumsplit  12177  geolim2  12198  cvgratnnlemseq  12212  cvgratz  12218  ef0lem  12346  efcj  12359  ef4p  12380  efgt1p  12382  tanval3ap  12400  efi4p  12403  sinadd  12422  cosadd  12423  tanaddap  12425  addsin  12428  demoivreALT  12460  opoe  12581  pythagtriplem4  12966  pythagtriplem12  12973  gzaddcl  13075  cncrng  14717  addccncf  15465  dvaddxxbr  15566  dvaddxx  15568  dviaddf  15570  dveflem  15591  plyaddcl  15619  plymulcl  15620  plysubcl  15621  sinperlem  15673  ptolemy  15689  tangtx  15703  sinkpi  15712  binom4  15844  lgsquad2lem1  15954  2sqlem2  15988