Theorem addcli 11189

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 11156	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 702	1 ⊢ (𝐴 + 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7397  ℂcc 11072   + caddc 11077

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  eqneg  11912  2cn  12294  3cn  12300  4cn  12304  5cn  12307  6cn  12310  7cn  12313  8cn  12316  9cn  12319  nummac  12739  binom2i  14226  sqeqori  14228  crreczi  14242  nn0opthlem1  14282  nn0opth2i  14285  3dvds2dec  16368  mod2xnegi  17108  karatsuba  17120  pige3ALT  26586  eff1o  26615  1cubrlem  26907  1cubr  26908  bposlem8  27356  ax5seglem7  29137  ipidsq  30914  ip1ilem  31030  pythi  31054  normlem2  31315  normlem3  31316  normlem7  31320  normlem9  31322  bcseqi  31324  norm-ii-i  31341  normpythi  31346  normpari  31358  polid2i  31361  lnopunilem1  32214  lnophmlem2  32221  dpmul100  33075  dpadd3  33090  dpmul4  33092  cos9thpiminplylem4  34083  cos9thpiminplylem5  34084  ballotlem2  34787  hgt750lem2  34947  quad3  36021  faclimlem1  36094  itg2addnclem3  38173  sqmid3api  42893  235t711  42915  sn-0tie0  43074  fltnltalem  43245  areaquad  43794  resqrtvalex  44222  imsqrtvalex  44223  fourierswlem  46805  fouriersw  46806  2t6m3t4e0  48971