Theorem addcl 8135

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6007   CCcc 8008   + caddc 8013

This theorem was proved from axioms:  ax-addcl 8106

This theorem is referenced by:  adddir  8148  0cn  8149  addcli  8161  addcld  8177  muladd11  8290  peano2cn  8292  muladd11r  8313  add4  8318  cnegexlem3  8334  cnegex  8335  0cnALT  8347  negeu  8348  pncan  8363  2addsub  8371  addsubeq4  8372  nppcan2  8388  ppncan  8399  muladd  8541  mulsub  8558  recexap  8811  muleqadd  8826  conjmulap  8887  ofnegsub  9120  halfaddsubcl  9355  halfaddsub  9356  serf  10717  ser3add  10756  ser3sub  10757  ser0  10767  binom2  10885  binom3  10891  bernneq  10894  lswccatn0lsw  11159  shftlem  11342  shftval2  11352  shftval5  11355  2shfti  11357  crre  11383  crim  11384  cjadd  11410  addcj  11417  sqabsadd  11581  absreimsq  11593  absreim  11594  abstri  11630  addcn2  11836  climadd  11852  clim2ser  11863  clim2ser2  11864  isermulc2  11866  serf0  11878  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsum3  11913  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumcl  11926  sumsnf  11935  fsummulc2  11974  binom  12010  isumshft  12016  isumsplit  12017  geolim2  12038  cvgratnnlemseq  12052  cvgratz  12058  ef0lem  12186  efcj  12199  ef4p  12220  efgt1p  12222  tanval3ap  12240  efi4p  12243  sinadd  12262  cosadd  12263  tanaddap  12265  addsin  12268  demoivreALT  12300  opoe  12421  pythagtriplem4  12806  pythagtriplem12  12813  gzaddcl  12915  cncrng  14548  addccncf  15289  dvaddxxbr  15390  dvaddxx  15392  dviaddf  15394  dveflem  15415  plyaddcl  15443  plymulcl  15444  plysubcl  15445  sinperlem  15497  ptolemy  15513  tangtx  15527  sinkpi  15536  binom4  15668  lgsquad2lem1  15775  2sqlem2  15809