Theorem addcli 10044

Description: Closure law for addition. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC

Assertion

Ref	Expression
addcli	|- ( A + B ) e. CC

Proof of Theorem addcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		addcl 10018	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1, 2, 3	mp2an 708	1 |- ( A + B ) e. CC

Syntax hints:   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9996

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  eqneg  10745  nummac  11558  binom2i  12974  sqeqori  12976  crreczi  12989  nn0opthlem1  13055  nn0opth2i  13058  3dvds2dec  15056  3dvds2decOLD  15057  mod2xnegi  15775  karatsuba  15792  karatsubaOLD  15793  pige3  24269  eff1o  24295  1cubrlem  24568  1cubr  24569  bposlem8  25016  ax5seglem7  25815  ipidsq  27565  ip1ilem  27681  pythi  27705  normlem2  27968  normlem3  27969  normlem7  27973  normlem9  27975  bcseqi  27977  norm-ii-i  27994  normpythi  27999  normpari  28011  polid2i  28014  lnopunilem1  28869  lnophmlem2  28876  dpmul100  29605  dpadd3  29620  dpmul4  29622  ballotlem2  30550  hgt750lem2  30730  quad3  31564  faclimlem1  31629  itg2addnclem3  33463  areaquad  37802  fourierswlem  40447  fouriersw  40448  2t6m3t4e0  42126