MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcli Structured version   Visualization version   GIF version

Theorem addcli 10335
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
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 addcl 10306 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 684 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  (class class class)co 6878  cc 10222   + caddc 10227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10284
This theorem depends on definitions:  df-bi 199  df-an 386
This theorem is referenced by:  eqneg  11037  2cn  11388  3cn  11394  4cn  11399  5cn  11403  6cn  11407  7cn  11411  8cn  11415  9cn  11419  nummac  11829  binom2i  13228  sqeqori  13230  crreczi  13243  nn0opthlem1  13308  nn0opth2i  13311  3dvds2dec  15393  mod2xnegi  16108  karatsuba  16121  pige3  24611  eff1o  24637  1cubrlem  24920  1cubr  24921  bposlem8  25368  ax5seglem7  26172  ipidsq  28090  ip1ilem  28206  pythi  28230  normlem2  28493  normlem3  28494  normlem7  28498  normlem9  28500  bcseqi  28502  norm-ii-i  28519  normpythi  28524  normpari  28536  polid2i  28539  lnopunilem1  29394  lnophmlem2  29401  dpmul100  30121  dpadd3  30136  dpmul4  30138  ballotlem2  31067  hgt750lem2  31250  quad3  32079  faclimlem1  32143  itg2addnclem3  33951  sqmid3api  37994  235t711  38002  areaquad  38586  fourierswlem  41190  fouriersw  41191  2t6m3t4e0  42925
  Copyright terms: Public domain W3C validator