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

Theorem addcli 10385
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 10356 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 682 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 6924  cc 10272   + caddc 10277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10334
This theorem depends on definitions:  df-bi 199  df-an 387
This theorem is referenced by:  eqneg  11097  2cn  11454  3cn  11460  4cn  11465  5cn  11469  6cn  11473  7cn  11477  8cn  11481  9cn  11485  nummac  11895  binom2i  13297  sqeqori  13299  crreczi  13312  nn0opthlem1  13377  nn0opth2i  13380  3dvds2dec  15465  mod2xnegi  16183  karatsuba  16196  pige3  24711  eff1o  24737  1cubrlem  25023  1cubr  25024  bposlem8  25472  ax5seglem7  26288  ipidsq  28141  ip1ilem  28257  pythi  28281  normlem2  28544  normlem3  28545  normlem7  28549  normlem9  28551  bcseqi  28553  norm-ii-i  28570  normpythi  28575  normpari  28587  polid2i  28590  lnopunilem1  29445  lnophmlem2  29452  dpmul100  30171  dpadd3  30186  dpmul4  30188  ballotlem2  31153  hgt750lem2  31336  quad3  32165  faclimlem1  32227  itg2addnclem3  34093  sqmid3api  38155  235t711  38163  areaquad  38770  fourierswlem  41384  fouriersw  41385  2t6m3t4e0  43151
  Copyright terms: Public domain W3C validator