Theorem adddii 8337

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 8312	. 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 6085   CCcc 8178   + caddc 8183   x. cmul 8185

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 8284

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

This theorem is used by:  3t3e9  9466  numltc  9812  numsucc  9826  numma  9830  decmul10add  9855  4t3lem  9883  9t11e99  9916  decbin2  9927  binom2i  11100  3dec  11168  3dvds2dec  12652  mod2xnegi  13221  decsplit  13232  log2ublem1  16182  log2ublem2  16183  bposlem8  16279