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

Theorem adddii 10389
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 10361 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1534 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  wcel 2106  (class class class)co 6922  cc 10270   + caddc 10275   · cmul 10277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10339
This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073
This theorem is referenced by:  addid1  10556  3t3e9  11549  numltc  11872  numsucc  11886  numma  11890  decmul10add  11916  4t3lem  11944  9t11e99  11977  decbin2  11988  binom2i  13293  3dec  13371  faclbnd4lem1  13398  3dvds2dec  15461  mod2xnegi  16179  decsplit  16191  log2ublem1  25125  log2ublem2  25126  bposlem8  25468  ax5seglem7  26284  ip0i  28266  ip1ilem  28267  ipasslem10  28280  normlem0  28552  polid2i  28600  lnopunilem1  29455  dfdec100  30154  dpmul10  30179  dpmul  30197  dpmul4  30198  sqmid3api  38141  fourierswlem  41366  3exp4mod41  42546  2t6m3t4e0  43133
  Copyright terms: Public domain W3C validator