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

Theorem addcli 10625
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 10597 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 690 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  (class class class)co 7133  cc 10513   + caddc 10518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10575
This theorem depends on definitions:  df-bi 209  df-an 399
This theorem is referenced by:  eqneg  11338  2cn  11691  3cn  11697  4cn  11701  5cn  11704  6cn  11707  7cn  11710  8cn  11713  9cn  11716  nummac  12122  binom2i  13559  sqeqori  13561  crreczi  13574  nn0opthlem1  13613  nn0opth2i  13616  3dvds2dec  15662  mod2xnegi  16385  karatsuba  16398  pige3ALT  25091  eff1o  25120  1cubrlem  25406  1cubr  25407  bposlem8  25854  ax5seglem7  26708  ipidsq  28472  ip1ilem  28588  pythi  28612  normlem2  28873  normlem3  28874  normlem7  28878  normlem9  28880  bcseqi  28882  norm-ii-i  28899  normpythi  28904  normpari  28916  polid2i  28919  lnopunilem1  29772  lnophmlem2  29779  dpmul100  30560  dpadd3  30575  dpmul4  30577  ballotlem2  31754  hgt750lem2  31931  quad3  32921  faclimlem1  32983  itg2addnclem3  34986  sqmid3api  39289  235t711  39297  fltnltalem  39411  areaquad  39959  fourierswlem  42663  fouriersw  42664  2t6m3t4e0  44541
  Copyright terms: Public domain W3C validator