Theorem adddid 7814

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647   x. cmul 7649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-distr 7748

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  subdi  8171  mulreim  8390  apadd1  8394  conjmulap  8513  cju  8743  flhalf  10106  modqcyc  10163  addmodlteq  10202  binom2  10434  binom3  10440  sqoddm1div8  10475  bcpasc  10544  remim  10664  mulreap  10668  readd  10673  remullem  10675  imadd  10681  cjadd  10688  bdtrilem  11042  fsummulc2  11249  binomlem  11284  tanval3ap  11457  sinadd  11479  tanaddap  11482  bezoutlemnewy  11720  dvdsmulgcd  11749  lcmgcdlem  11794  tangtx  12967  rpmulcxp  13038