Theorem adddid 8356

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 8317	. 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 ) ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   + caddc 8188   x. cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8289

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

This theorem is used by:  subdi  8719  mulreim  8940  apadd1  8944  conjmulap  9067  cju  9299  flhalf  10757  modqcyc  10816  addmodlteq  10855  binom2  11108  binom3  11114  sqoddm1div8  11151  bcpasc  11225  hashf1lem2  11307  remim  11646  mulreap  11650  readd  11655  remullem  11657  imadd  11663  cjadd  11670  bdtrilem  12029  fsummulc2  12239  binomlem  12274  tanval3ap  12505  sinadd  12527  tanaddap  12530  bezoutlemnewy  12797  dvdsmulgcd  12826  lcmgcdlem  12879  pythagtriplem1  13072  pcaddlem  13146  mul4sqlem  13200  tangtx  16082  rpmulcxp  16159  rpcxpmul2  16163  binom4  16236  chtqub  16313  bposlem9  16336  lgseisenlem2  16412  2lgsoddprmlem2  16447  2sqlem4  16459  2sqlem8  16464