Theorem adddid 8340

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 8301	. 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 1278	1 |- ( ph -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172   x. cmul 8174

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 8273

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

This theorem is referenced by:  subdi  8702  mulreim  8922  apadd1  8926  conjmulap  9049  cju  9281  flhalf  10715  modqcyc  10774  addmodlteq  10813  binom2  11066  binom3  11072  sqoddm1div8  11109  bcpasc  11182  hashf1lem2  11264  remim  11603  mulreap  11607  readd  11612  remullem  11614  imadd  11620  cjadd  11627  bdtrilem  11983  fsummulc2  12193  binomlem  12228  tanval3ap  12459  sinadd  12481  tanaddap  12484  bezoutlemnewy  12751  dvdsmulgcd  12780  lcmgcdlem  12833  pythagtriplem1  13022  pcaddlem  13096  mul4sqlem  13150  tangtx  15862  rpmulcxp  15934  rpcxpmul2  15938  binom4  16004  lgseisenlem2  16104  2lgsoddprmlem2  16139  2sqlem4  16151  2sqlem8  16156