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  9817  numsucc  9831  numma  9835  decmul10add  9860  4t3lem  9888  9t11e99  9921  decbin2  9932  binom2i  11105  3dec  11173  3dvds2dec  12657  mod2xnegi  13226  decsplit  13237  log2ublem1  16238  log2ublem2  16239  bposlem8  16335