Theorem addcli 11296

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187

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

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

This theorem is referenced by:  eqneg  12014  2cn  12368  3cn  12374  4cn  12378  5cn  12381  6cn  12384  7cn  12387  8cn  12390  9cn  12393  nummac  12803  binom2i  14261  sqeqori  14263  crreczi  14277  nn0opthlem1  14317  nn0opth2i  14320  3dvds2dec  16381  mod2xnegi  17118  karatsuba  17131  pige3ALT  26580  eff1o  26609  1cubrlem  26902  1cubr  26903  bposlem8  27353  ax5seglem7  28968  ipidsq  30742  ip1ilem  30858  pythi  30882  normlem2  31143  normlem3  31144  normlem7  31148  normlem9  31150  bcseqi  31152  norm-ii-i  31169  normpythi  31174  normpari  31186  polid2i  31189  lnopunilem1  32042  lnophmlem2  32049  dpmul100  32861  dpadd3  32876  dpmul4  32878  ballotlem2  34453  hgt750lem2  34629  quad3  35638  faclimlem1  35705  itg2addnclem3  37633  sqmid3api  42272  235t711  42293  sn-0tie0  42415  fltnltalem  42617  areaquad  43177  resqrtvalex  43607  imsqrtvalex  43608  fourierswlem  46151  fouriersw  46152  2t6m3t4e0  48073