Theorem addcli 11328

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7430  ℂcc 11211   + caddc 11216

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11273

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  eqneg  12050  2cn  12431  3cn  12437  4cn  12441  5cn  12444  6cn  12447  7cn  12450  8cn  12453  9cn  12456  nummac  12877  binom2i  14369  sqeqori  14371  crreczi  14385  nn0opthlem1  14425  nn0opth2i  14428  3dvds2dec  16518  mod2xnegi  17264  karatsuba  17276  pige3ALT  26863  eff1o  26892  1cubrlem  27184  1cubr  27185  bposlem8  27633  ax5seglem7  29528  ipidsq  31327  ip1ilem  31443  pythi  31467  normlem2  31728  normlem3  31729  normlem7  31733  normlem9  31735  bcseqi  31737  norm-ii-i  31754  normpythi  31759  normpari  31771  polid2i  31774  lnopunilem1  32627  lnophmlem2  32634  dpmul100  33519  dpadd3  33534  dpmul4  33536  cos9thpiminplylem4  34473  cos9thpiminplylem5  34474  ballotlem2  35177  hgt750lem2  35337  quad3  36559  faclimlem1  36638  itg2addnclem3  38734  25or6to4  43399  sqmid3api  43483  235t711  43505  sn-0tie0  43658  fltnltalem  43816  areaquad  44361  resqrtvalex  44788  imsqrtvalex  44789  fourierswlem  47382  fouriersw  47383  goldpolyfactor  48069  goldratmolem3  48076  goldratmolem4  48077  goldratval  48078  2t6m3t4e0  49602