Theorem adddii 10050

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 10025	. 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 1424	1 |- ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) )

Syntax hints:   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10003

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  addid1  10216  3t3e9  11180  numltc  11528  numsucc  11549  numma  11557  decmul10add  11593  decmul10addOLD  11594  4t3lem  11631  9t11e99  11671  9t11e99OLD  11672  decbin2  11683  binom2i  12974  3dec  13050  3decOLD  13053  faclbnd4lem1  13080  3dvds2dec  15056  3dvds2decOLD  15057  mod2xnegi  15775  decsplit  15787  decsplitOLD  15791  log2ublem1  24673  log2ublem2  24674  bposlem8  25016  ax5seglem7  25815  ip0i  27680  ip1ilem  27681  ipasslem10  27694  normlem0  27966  polid2i  28014  lnopunilem1  28869  dfdec100  29576  dpmul10  29603  dpmul  29621  dpmul4  29622  fourierswlem  40447  3exp4mod41  41533  2t6m3t4e0  42126