Theorem adddid 7783

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616   x. cmul 7618

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  subdi  8140  mulreim  8359  apadd1  8363  conjmulap  8482  cju  8712  flhalf  10068  modqcyc  10125  addmodlteq  10164  binom2  10396  binom3  10402  sqoddm1div8  10437  bcpasc  10505  remim  10625  mulreap  10629  readd  10634  remullem  10636  imadd  10642  cjadd  10649  bdtrilem  11003  fsummulc2  11210  binomlem  11245  tanval3ap  11410  sinadd  11432  tanaddap  11435  bezoutlemnewy  11673  dvdsmulgcd  11702  lcmgcdlem  11747  tangtx  12908