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

Theorem addcli 10635
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 10607 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 688 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10585
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  eqneg  11348  2cn  11700  3cn  11706  4cn  11710  5cn  11713  6cn  11716  7cn  11719  8cn  11722  9cn  11725  nummac  12131  binom2i  13562  sqeqori  13564  crreczi  13577  nn0opthlem1  13616  nn0opth2i  13619  3dvds2dec  15670  mod2xnegi  16395  karatsuba  16408  pige3ALT  25032  eff1o  25060  1cubrlem  25346  1cubr  25347  bposlem8  25794  ax5seglem7  26648  ipidsq  28414  ip1ilem  28530  pythi  28554  normlem2  28815  normlem3  28816  normlem7  28820  normlem9  28822  bcseqi  28824  norm-ii-i  28841  normpythi  28846  normpari  28858  polid2i  28861  lnopunilem1  29714  lnophmlem2  29721  dpmul100  30500  dpadd3  30515  dpmul4  30517  ballotlem2  31645  hgt750lem2  31822  quad3  32810  faclimlem1  32872  itg2addnclem3  34826  sqmid3api  39047  235t711  39055  fltnltalem  39152  areaquad  39701  fourierswlem  42392  fouriersw  42393  2t6m3t4e0  44324
  Copyright terms: Public domain W3C validator