Theorem addcl 7874

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2136  (class class class)co 5841   CCcc 7747   + caddc 7752

This theorem was proved from axioms:  ax-addcl 7845

This theorem is referenced by:  adddir  7886  0cn  7887  addcli  7899  addcld  7914  muladd11  8027  peano2cn  8029  muladd11r  8050  add4  8055  cnegexlem3  8071  cnegex  8072  0cnALT  8084  negeu  8085  pncan  8100  2addsub  8108  addsubeq4  8109  nppcan2  8125  ppncan  8136  muladd  8278  mulsub  8295  recexap  8546  muleqadd  8561  conjmulap  8621  halfaddsubcl  9086  halfaddsub  9087  serf  10405  ser3add  10436  ser3sub  10437  ser0  10445  binom2  10562  binom3  10568  bernneq  10571  shftlem  10754  shftval2  10764  shftval5  10767  2shfti  10769  crre  10795  crim  10796  cjadd  10822  addcj  10829  sqabsadd  10993  absreimsq  11005  absreim  11006  abstri  11042  addcn2  11247  climadd  11263  clim2ser  11274  clim2ser2  11275  isermulc2  11277  serf0  11289  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  zsumdc  11321  fsum3  11324  fsum3cvg2  11331  fsum3ser  11334  fsumcl2lem  11335  fsumcl  11337  sumsnf  11346  fsummulc2  11385  binom  11421  isumshft  11427  isumsplit  11428  geolim2  11449  cvgratnnlemseq  11463  cvgratz  11469  ef0lem  11597  efcj  11610  ef4p  11631  efgt1p  11633  tanval3ap  11651  efi4p  11654  sinadd  11673  cosadd  11674  tanaddap  11676  addsin  11679  demoivreALT  11710  opoe  11828  pythagtriplem4  12196  pythagtriplem12  12203  gzaddcl  12303  addccncf  13186  dvaddxxbr  13265  dvaddxx  13267  dviaddf  13269  dveflem  13287  sinperlem  13329  ptolemy  13345  tangtx  13359  sinkpi  13368  binom4  13497  2sqlem2  13551