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

Theorem adddiri 10642
Description: Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
axi.3 𝐶 ∈ ℂ
Assertion
Ref Expression
adddiri ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))

Proof of Theorem adddiri
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 axi.3 . 2 𝐶 ∈ ℂ
4 adddir 10620 . 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-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-addcl 10585  ax-mulcom 10589  ax-distr 10592
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  numma  12130  binom2i  13562  3dvdsdec  15669  3dvds2dec  15670  dec5nprm  16390  dec2nprm  16391  mod2xnegi  16395  karatsuba  16408  sincosq3sgn  25013  sincosq4sgn  25014  ang180lem2  25315  1cubrlem  25346  bposlem8  25794  2lgsoddprmlem3c  25915  2lgsoddprmlem3d  25916  normlem3  28816  dpmul100  30500  dpmul1000  30502  dpadd3  30515  dpmul4  30517  problem2  32806  areaquad  39701  tgoldbachlt  43858
  Copyright terms: Public domain W3C validator