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

Theorem adddii 10641
Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
axi.3 𝐶 ∈ ℂ
Assertion
Ref Expression
adddii (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))

Proof of Theorem adddii
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 axi.3 . 2 𝐶 ∈ ℂ
4 adddi 10614 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1452 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10592
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081
This theorem is referenced by:  addid1  10808  3t3e9  11792  numltc  12112  numsucc  12126  numma  12130  decmul10add  12155  4t3lem  12183  9t11e99  12216  decbin2  12227  binom2i  13562  3dec  13614  faclbnd4lem1  13641  3dvds2dec  15670  mod2xnegi  16395  decsplit  16407  log2ublem1  25451  log2ublem2  25452  bposlem8  25794  ax5seglem7  26648  ip0i  28529  ip1ilem  28530  ipasslem10  28543  normlem0  28813  polid2i  28861  lnopunilem1  29714  dfdec100  30473  dpmul10  30498  dpmul  30516  dpmul4  30517  sn-1ne2  39036  sqmid3api  39047  fourierswlem  42392  3exp4mod41  43658  2t6m3t4e0  44324
  Copyright terms: Public domain W3C validator