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

Theorem addcli 10041
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 10015 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 708 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  (class class class)co 6647  cc 9931   + caddc 9936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9993
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  eqneg  10742  nummac  11555  binom2i  12969  sqeqori  12971  crreczi  12984  nn0opthlem1  13050  nn0opth2i  13053  3dvds2dec  15050  3dvds2decOLD  15051  mod2xnegi  15769  karatsuba  15786  karatsubaOLD  15787  pige3  24263  eff1o  24289  1cubrlem  24562  1cubr  24563  bposlem8  25010  ax5seglem7  25809  ipidsq  27549  ip1ilem  27665  pythi  27689  normlem2  27952  normlem3  27953  normlem7  27957  normlem9  27959  bcseqi  27961  norm-ii-i  27978  normpythi  27983  normpari  27995  polid2i  27998  lnopunilem1  28853  lnophmlem2  28860  dpmul100  29590  dpadd3  29605  dpmul4  29607  ballotlem2  30535  hgt750lem2  30715  quad3  31549  faclimlem1  31615  itg2addnclem3  33443  areaquad  37628  fourierswlem  40216  fouriersw  40217  2t6m3t4e0  41897
  Copyright terms: Public domain W3C validator