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  11069  shftval2  11079  shftval5  11082  2shfti  11084  crre  11110  crim  11111  cjadd  11137  addcj  11144  sqabsadd  11308  absreimsq  11320  absreim  11321  abstri  11357  addcn2  11563  climadd  11579  clim2ser  11590  clim2ser2  11591  isermulc2  11593  serf0  11605  sumrbdclem  11630  fsum3cvg  11631  summodclem3  11633  summodclem2a  11634  zsumdc  11637  fsum3  11640  fsum3cvg2  11647  fsum3ser  11650  fsumcl2lem  11651  fsumcl  11653  sumsnf  11662  fsummulc2  11701  binom  11737  isumshft  11743  isumsplit  11744  geolim2  11765  cvgratnnlemseq  11779  cvgratz  11785  ef0lem  11913  efcj  11926  ef4p  11947  efgt1p  11949  tanval3ap  11967  efi4p  11970  sinadd  11989  cosadd  11990  tanaddap  11992  addsin  11995  demoivreALT  12027  opoe  12148  pythagtriplem4  12533  pythagtriplem12  12540  gzaddcl  12642  cncrng  14273  addccncf  15014  dvaddxxbr  15115  dvaddxx  15117  dviaddf  15119  dveflem  15140  plyaddcl  15168  plymulcl  15169  plysubcl  15170  sinperlem  15222  ptolemy  15238  tangtx  15252  sinkpi  15261  binom4  15393  lgsquad2lem1  15500  2sqlem2  15534