Theorem addcl 8049

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175  (class class class)co 5943   CCcc 7922   + caddc 7927

This theorem was proved from axioms:  ax-addcl 8020

This theorem is referenced by:  adddir  8062  0cn  8063  addcli  8075  addcld  8091  muladd11  8204  peano2cn  8206  muladd11r  8227  add4  8232  cnegexlem3  8248  cnegex  8249  0cnALT  8261  negeu  8262  pncan  8277  2addsub  8285  addsubeq4  8286  nppcan2  8302  ppncan  8313  muladd  8455  mulsub  8472  recexap  8725  muleqadd  8740  conjmulap  8801  ofnegsub  9034  halfaddsubcl  9269  halfaddsub  9270  serf  10626  ser3add  10665  ser3sub  10666  ser0  10676  binom2  10794  binom3  10800  bernneq  10803  lswccatn0lsw  11065  shftlem  11098  shftval2  11108  shftval5  11111  2shfti  11113  crre  11139  crim  11140  cjadd  11166  addcj  11173  sqabsadd  11337  absreimsq  11349  absreim  11350  abstri  11386  addcn2  11592  climadd  11608  clim2ser  11619  clim2ser2  11620  isermulc2  11622  serf0  11634  sumrbdclem  11659  fsum3cvg  11660  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsum3  11669  fsum3cvg2  11676  fsum3ser  11679  fsumcl2lem  11680  fsumcl  11682  sumsnf  11691  fsummulc2  11730  binom  11766  isumshft  11772  isumsplit  11773  geolim2  11794  cvgratnnlemseq  11808  cvgratz  11814  ef0lem  11942  efcj  11955  ef4p  11976  efgt1p  11978  tanval3ap  11996  efi4p  11999  sinadd  12018  cosadd  12019  tanaddap  12021  addsin  12024  demoivreALT  12056  opoe  12177  pythagtriplem4  12562  pythagtriplem12  12569  gzaddcl  12671  cncrng  14302  addccncf  15043  dvaddxxbr  15144  dvaddxx  15146  dviaddf  15148  dveflem  15169  plyaddcl  15197  plymulcl  15198  plysubcl  15199  sinperlem  15251  ptolemy  15267  tangtx  15281  sinkpi  15290  binom4  15422  lgsquad2lem1  15529  2sqlem2  15563