Theorem adddid 8132

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )
addassd.3	|- ( ph -> C e. CC )

Assertion

Ref	Expression
adddid	|- ( ph -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		addassd.3	. 2 |- ( ph -> C e. CC )
4		adddi 8092	. 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	syl3anc 1250	1 |- ( ph -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178  (class class class)co 5967   CCcc 7958   + caddc 7963   x. cmul 7965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8064

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  subdi  8492  mulreim  8712  apadd1  8716  conjmulap  8837  cju  9069  flhalf  10482  modqcyc  10541  addmodlteq  10580  binom2  10833  binom3  10839  sqoddm1div8  10875  bcpasc  10948  remim  11286  mulreap  11290  readd  11295  remullem  11297  imadd  11303  cjadd  11310  bdtrilem  11665  fsummulc2  11874  binomlem  11909  tanval3ap  12140  sinadd  12162  tanaddap  12165  bezoutlemnewy  12432  dvdsmulgcd  12461  lcmgcdlem  12514  pythagtriplem1  12703  pcaddlem  12777  mul4sqlem  12831  tangtx  15425  rpmulcxp  15496  rpcxpmul2  15500  binom4  15566  lgseisenlem2  15663  2lgsoddprmlem2  15698  2sqlem4  15710  2sqlem8  15715