Theorem adddid 8298

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130   x. cmul 8132

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 8231

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

This theorem is referenced by:  subdi  8658  mulreim  8878  apadd1  8882  conjmulap  9003  cju  9235  flhalf  10662  modqcyc  10721  addmodlteq  10760  binom2  11013  binom3  11019  sqoddm1div8  11055  bcpasc  11128  remim  11545  mulreap  11549  readd  11554  remullem  11556  imadd  11562  cjadd  11569  bdtrilem  11924  fsummulc2  12134  binomlem  12169  tanval3ap  12400  sinadd  12422  tanaddap  12425  bezoutlemnewy  12692  dvdsmulgcd  12721  lcmgcdlem  12774  pythagtriplem1  12963  pcaddlem  13037  mul4sqlem  13091  tangtx  15703  rpmulcxp  15774  rpcxpmul2  15778  binom4  15844  lgseisenlem2  15944  2lgsoddprmlem2  15979  2sqlem4  15991  2sqlem8  15996