Theorem adddid 8350

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 8311	. 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 6085   CCcc 8177   + caddc 8182   x. cmul 8184

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 8283

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

This theorem is used by:  subdi  8713  mulreim  8934  apadd1  8938  conjmulap  9061  cju  9293  flhalf  10750  modqcyc  10809  addmodlteq  10848  binom2  11101  binom3  11107  sqoddm1div8  11144  bcpasc  11218  hashf1lem2  11300  remim  11639  mulreap  11643  readd  11648  remullem  11650  imadd  11656  cjadd  11663  bdtrilem  12021  fsummulc2  12231  binomlem  12266  tanval3ap  12497  sinadd  12519  tanaddap  12522  bezoutlemnewy  12789  dvdsmulgcd  12818  lcmgcdlem  12871  pythagtriplem1  13064  pcaddlem  13138  mul4sqlem  13192  tangtx  15989  rpmulcxp  16064  rpcxpmul2  16068  binom4  16138  lgseisenlem2  16288  2lgsoddprmlem2  16323  2sqlem4  16335  2sqlem8  16340