Theorem adddid 8097

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   + caddc 7928   x. cmul 7930

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  subdi  8457  mulreim  8677  apadd1  8681  conjmulap  8802  cju  9034  flhalf  10445  modqcyc  10504  addmodlteq  10543  binom2  10796  binom3  10802  sqoddm1div8  10838  bcpasc  10911  remim  11171  mulreap  11175  readd  11180  remullem  11182  imadd  11188  cjadd  11195  bdtrilem  11550  fsummulc2  11759  binomlem  11794  tanval3ap  12025  sinadd  12047  tanaddap  12050  bezoutlemnewy  12317  dvdsmulgcd  12346  lcmgcdlem  12399  pythagtriplem1  12588  pcaddlem  12662  mul4sqlem  12716  tangtx  15310  rpmulcxp  15381  rpcxpmul2  15385  binom4  15451  lgseisenlem2  15548  2lgsoddprmlem2  15583  2sqlem4  15595  2sqlem8  15600