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

Theorem adddiri 10243
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 10223 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1573 1 ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  (class class class)co 6813  cc 10126   + caddc 10131   · cmul 10133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-addcl 10188  ax-mulcom 10192  ax-distr 10195
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816
This theorem is referenced by:  numma  11749  binom2i  13168  3dvdsdec  15256  3dvdsdecOLD  15257  3dvds2dec  15258  3dvds2decOLD  15259  dec5nprm  15972  dec2nprm  15973  mod2xnegi  15977  karatsuba  15994  karatsubaOLD  15995  sincosq3sgn  24451  sincosq4sgn  24452  ang180lem2  24739  1cubrlem  24767  bposlem8  25215  2lgsoddprmlem3c  25336  2lgsoddprmlem3d  25337  normlem3  28278  dpmul100  29914  dpmul1000  29916  dpadd3  29929  dpmul4  29931  problem2  31866  problem2OLD  31867  areaquad  38304  tgoldbachlt  42214  tgoldbachltOLD  42220
  Copyright terms: Public domain W3C validator