Theorem addcl 7888

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2141  (class class class)co 5851   CCcc 7761   + caddc 7766

This theorem was proved from axioms:  ax-addcl 7859

This theorem is referenced by:  adddir  7900  0cn  7901  addcli  7913  addcld  7928  muladd11  8041  peano2cn  8043  muladd11r  8064  add4  8069  cnegexlem3  8085  cnegex  8086  0cnALT  8098  negeu  8099  pncan  8114  2addsub  8122  addsubeq4  8123  nppcan2  8139  ppncan  8150  muladd  8292  mulsub  8309  recexap  8560  muleqadd  8575  conjmulap  8635  halfaddsubcl  9100  halfaddsub  9101  serf  10419  ser3add  10450  ser3sub  10451  ser0  10459  binom2  10576  binom3  10582  bernneq  10585  shftlem  10769  shftval2  10779  shftval5  10782  2shfti  10784  crre  10810  crim  10811  cjadd  10837  addcj  10844  sqabsadd  11008  absreimsq  11020  absreim  11021  abstri  11057  addcn2  11262  climadd  11278  clim2ser  11289  clim2ser2  11290  isermulc2  11292  serf0  11304  sumrbdclem  11329  fsum3cvg  11330  summodclem3  11332  summodclem2a  11333  zsumdc  11336  fsum3  11339  fsum3cvg2  11346  fsum3ser  11349  fsumcl2lem  11350  fsumcl  11352  sumsnf  11361  fsummulc2  11400  binom  11436  isumshft  11442  isumsplit  11443  geolim2  11464  cvgratnnlemseq  11478  cvgratz  11484  ef0lem  11612  efcj  11625  ef4p  11646  efgt1p  11648  tanval3ap  11666  efi4p  11669  sinadd  11688  cosadd  11689  tanaddap  11691  addsin  11694  demoivreALT  11725  opoe  11843  pythagtriplem4  12211  pythagtriplem12  12218  gzaddcl  12318  addccncf  13341  dvaddxxbr  13420  dvaddxx  13422  dviaddf  13424  dveflem  13442  sinperlem  13484  ptolemy  13500  tangtx  13514  sinkpi  13523  binom4  13652  2sqlem2  13706