Theorem adddid 8204

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 8164	. 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 6018   CCcc 8030   + caddc 8035   x. cmul 8037

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 8136

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

This theorem is referenced by:  subdi  8564  mulreim  8784  apadd1  8788  conjmulap  8909  cju  9141  flhalf  10563  modqcyc  10622  addmodlteq  10661  binom2  10914  binom3  10920  sqoddm1div8  10956  bcpasc  11029  remim  11438  mulreap  11442  readd  11447  remullem  11449  imadd  11455  cjadd  11462  bdtrilem  11817  fsummulc2  12027  binomlem  12062  tanval3ap  12293  sinadd  12315  tanaddap  12318  bezoutlemnewy  12585  dvdsmulgcd  12614  lcmgcdlem  12667  pythagtriplem1  12856  pcaddlem  12930  mul4sqlem  12984  tangtx  15581  rpmulcxp  15652  rpcxpmul2  15656  binom4  15722  lgseisenlem2  15819  2lgsoddprmlem2  15854  2sqlem4  15866  2sqlem8  15871