Theorem addcli 11220

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113

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

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

This theorem is referenced by:  eqneg  11934  2cn  12287  3cn  12293  4cn  12297  5cn  12300  6cn  12303  7cn  12306  8cn  12309  9cn  12312  nummac  12722  binom2i  14176  sqeqori  14178  crreczi  14191  nn0opthlem1  14228  nn0opth2i  14231  3dvds2dec  16276  mod2xnegi  17004  karatsuba  17017  pige3ALT  26029  eff1o  26058  1cubrlem  26346  1cubr  26347  bposlem8  26794  ax5seglem7  28224  ipidsq  29994  ip1ilem  30110  pythi  30134  normlem2  30395  normlem3  30396  normlem7  30400  normlem9  30402  bcseqi  30404  norm-ii-i  30421  normpythi  30426  normpari  30438  polid2i  30441  lnopunilem1  31294  lnophmlem2  31301  dpmul100  32094  dpadd3  32109  dpmul4  32111  ballotlem2  33518  hgt750lem2  33695  quad3  34686  faclimlem1  34744  itg2addnclem3  36589  sqmid3api  41243  235t711  41253  sn-0tie0  41360  fltnltalem  41452  areaquad  42013  resqrtvalex  42444  imsqrtvalex  42445  fourierswlem  44994  fouriersw  44995  2t6m3t4e0  47072