Theorem adddid 7937

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5851   CCcc 7765   + caddc 7770   x. cmul 7772

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 7871

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

This theorem is referenced by:  subdi  8297  mulreim  8516  apadd1  8520  conjmulap  8639  cju  8870  flhalf  10251  modqcyc  10308  addmodlteq  10347  binom2  10580  binom3  10586  sqoddm1div8  10622  bcpasc  10693  remim  10817  mulreap  10821  readd  10826  remullem  10828  imadd  10834  cjadd  10841  bdtrilem  11195  fsummulc2  11404  binomlem  11439  tanval3ap  11670  sinadd  11692  tanaddap  11695  bezoutlemnewy  11944  dvdsmulgcd  11973  lcmgcdlem  12024  pythagtriplem1  12212  pcaddlem  12285  mul4sqlem  12338  tangtx  13518  rpmulcxp  13589  binom4  13656  2sqlem4  13713  2sqlem8  13718