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  10758  modqcyc  10817  addmodlteq  10856  binom2  11109  binom3  11115  sqoddm1div8  11152  bcpasc  11226  hashf1lem2  11308  remim  11647  mulreap  11651  readd  11656  remullem  11658  imadd  11664  cjadd  11671  bdtrilem  12030  fsummulc2  12240  binomlem  12275  tanval3ap  12506  sinadd  12528  tanaddap  12531  bezoutlemnewy  12798  dvdsmulgcd  12827  lcmgcdlem  12880  pythagtriplem1  13073  pcaddlem  13147  mul4sqlem  13201  tangtx  16065  rpmulcxp  16142  rpcxpmul2  16146  binom4  16219  chtqub  16296  bposlem9  16319  lgseisenlem2  16395  2lgsoddprmlem2  16430  2sqlem4  16442  2sqlem8  16447