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

Theorem adddii 9994
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 9969 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1421 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  (class class class)co 6604  cc 9878   + caddc 9883   · cmul 9885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9947
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  addid1  10160  3t3e9  11124  numltc  11472  numsucc  11493  numma  11501  decmul10add  11537  decmul10addOLD  11538  4t3lem  11575  9t11e99  11615  9t11e99OLD  11616  decbin2  11627  binom2i  12914  3dec  12990  3decOLD  12993  faclbnd4lem1  13020  3dvds2dec  14980  3dvds2decOLD  14981  mod2xnegi  15699  decsplit  15711  decsplitOLD  15715  log2ublem1  24573  log2ublem2  24574  bposlem8  24916  ax5seglem7  25715  ip0i  27529  ip1ilem  27530  ipasslem10  27543  normlem0  27815  polid2i  27863  lnopunilem1  28718  fourierswlem  39754  3exp4mod41  40832  2t6m3t4e0  41414
  Copyright terms: Public domain W3C validator