Theorem addcli 11242

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

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
addcli	⊢ (𝐴 + 𝐵) ∈ ℂ

Proof of Theorem addcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		addcl 11212	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 + 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128   + caddc 11133

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

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  eqneg  11956  2cn  12309  3cn  12315  4cn  12319  5cn  12322  6cn  12325  7cn  12328  8cn  12331  9cn  12334  nummac  12744  binom2i  14199  sqeqori  14201  crreczi  14214  nn0opthlem1  14251  nn0opth2i  14254  3dvds2dec  16301  mod2xnegi  17031  karatsuba  17044  pige3ALT  26441  eff1o  26470  1cubrlem  26760  1cubr  26761  bposlem8  27211  ax5seglem7  28733  ipidsq  30507  ip1ilem  30623  pythi  30647  normlem2  30908  normlem3  30909  normlem7  30913  normlem9  30915  bcseqi  30917  norm-ii-i  30934  normpythi  30939  normpari  30951  polid2i  30954  lnopunilem1  31807  lnophmlem2  31814  dpmul100  32602  dpadd3  32617  dpmul4  32619  ballotlem2  34044  hgt750lem2  34220  quad3  35210  faclimlem1  35273  itg2addnclem3  37081  sqmid3api  41779  235t711  41789  sn-0tie0  41916  fltnltalem  42008  areaquad  42567  resqrtvalex  42998  imsqrtvalex  42999  fourierswlem  45541  fouriersw  45542  2t6m3t4e0  47335