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

Theorem adddiri 9402
Description: Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
axi.3  |-  C  e.  CC
Assertion
Ref Expression
adddiri  |-  ( ( A  +  B )  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C ) )

Proof of Theorem adddiri
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 axi.3 . 2  |-  C  e.  CC
4 adddir 9382 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1314 1  |-  ( ( A  +  B )  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756  (class class class)co 6096   CCcc 9285    + caddc 9290    x. cmul 9292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-addcl 9347  ax-mulcom 9351  ax-distr 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-iota 5386  df-fv 5431  df-ov 6099
This theorem is referenced by:  numma  10791  binom2i  11980  binom2aiOLD  11981  dec5nprm  14100  dec2nprm  14101  mod2xnegi  14105  karatsuba  14118  sincosq3sgn  21967  sincosq4sgn  21968  ang180lem2  22211  1cubrlem  22241  bposlem8  22635  normlem3  24519  problem2  27304  areaquad  29597
  Copyright terms: Public domain W3C validator