Theorem adddii 8342

Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC
axi.3	|- C e. CC

Assertion

Ref	Expression
adddii	|- ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) )

Proof of Theorem adddii

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		axi.3	. 2 |- C e. CC
4		adddi 8317	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
5	1, 2, 3, 4	mp3an 1378	1 |- ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) )

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   + caddc 8188   x. cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8289

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3t3e9  9472  numltc  9818  numsucc  9832  numma  9836  decmul10add  9861  4t3lem  9889  9t11e99  9922  decbin2  9933  binom2i  11106  3dec  11174  3dvds2dec  12658  mod2xnegi  13227  decsplit  13238  log2ublem1  16221  log2ublem2  16222  bposlem8  16318