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

Theorem addcli 11244
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 11214 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 691 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2099  (class class class)co 7414  cc 11130   + caddc 11135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11192
This theorem depends on definitions:  df-bi 206  df-an 396
This theorem is referenced by:  eqneg  11958  2cn  12311  3cn  12317  4cn  12321  5cn  12324  6cn  12327  7cn  12330  8cn  12333  9cn  12336  nummac  12746  binom2i  14201  sqeqori  14203  crreczi  14216  nn0opthlem1  14253  nn0opth2i  14256  3dvds2dec  16303  mod2xnegi  17033  karatsuba  17046  pige3ALT  26447  eff1o  26476  1cubrlem  26766  1cubr  26767  bposlem8  27217  ax5seglem7  28739  ipidsq  30513  ip1ilem  30629  pythi  30653  normlem2  30914  normlem3  30915  normlem7  30919  normlem9  30921  bcseqi  30923  norm-ii-i  30940  normpythi  30945  normpari  30957  polid2i  30960  lnopunilem1  31813  lnophmlem2  31820  dpmul100  32614  dpadd3  32629  dpmul4  32631  ballotlem2  34098  hgt750lem2  34274  quad3  35264  faclimlem1  35327  itg2addnclem3  37135  sqmid3api  41829  235t711  41839  sn-0tie0  41966  fltnltalem  42058  areaquad  42616  resqrtvalex  43047  imsqrtvalex  43048  fourierswlem  45590  fouriersw  45591  2t6m3t4e0  47384
  Copyright terms: Public domain W3C validator