Theorem adddid 8203

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034   x. cmul 8036

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 8135

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

This theorem is referenced by:  subdi  8563  mulreim  8783  apadd1  8787  conjmulap  8908  cju  9140  flhalf  10561  modqcyc  10620  addmodlteq  10659  binom2  10912  binom3  10918  sqoddm1div8  10954  bcpasc  11027  remim  11420  mulreap  11424  readd  11429  remullem  11431  imadd  11437  cjadd  11444  bdtrilem  11799  fsummulc2  12008  binomlem  12043  tanval3ap  12274  sinadd  12296  tanaddap  12299  bezoutlemnewy  12566  dvdsmulgcd  12595  lcmgcdlem  12648  pythagtriplem1  12837  pcaddlem  12911  mul4sqlem  12965  tangtx  15561  rpmulcxp  15632  rpcxpmul2  15636  binom4  15702  lgseisenlem2  15799  2lgsoddprmlem2  15834  2sqlem4  15846  2sqlem8  15851