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

Theorem addcli 9896
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 9870 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 703 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  (class class class)co 6523  cc 9786   + caddc 9791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9848
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  eqneg  10590  nummac  11386  binom2i  12787  sqeqori  12789  crreczi  12802  nn0opthlem1  12868  nn0opth2i  12871  3dvds2dec  14836  3dvds2decOLD  14837  mod2xnegi  15555  karatsuba  15572  karatsubaOLD  15573  pige3  23986  eff1o  24012  1cubrlem  24281  1cubr  24282  bposlem8  24729  ax5seglem7  25529  ipidsq  26749  ip1ilem  26867  pythi  26891  normlem2  27154  normlem3  27155  normlem7  27159  normlem9  27161  bcseqi  27163  norm-ii-i  27180  normpythi  27185  normpari  27197  polid2i  27200  lnopunilem1  28055  lnophmlem2  28062  ballotlem2  29679  quad3  30620  faclimlem1  30684  itg2addnclem3  32432  areaquad  36620  fourierswlem  38923  fouriersw  38924  2t6m3t4e0  41917
  Copyright terms: Public domain W3C validator