Theorem adddid 8099

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 8059	. 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 5946   CCcc 7925   + caddc 7930   x. cmul 7932

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 8031

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

This theorem is referenced by:  subdi  8459  mulreim  8679  apadd1  8683  conjmulap  8804  cju  9036  flhalf  10447  modqcyc  10506  addmodlteq  10545  binom2  10798  binom3  10804  sqoddm1div8  10840  bcpasc  10913  remim  11204  mulreap  11208  readd  11213  remullem  11215  imadd  11221  cjadd  11228  bdtrilem  11583  fsummulc2  11792  binomlem  11827  tanval3ap  12058  sinadd  12080  tanaddap  12083  bezoutlemnewy  12350  dvdsmulgcd  12379  lcmgcdlem  12432  pythagtriplem1  12621  pcaddlem  12695  mul4sqlem  12749  tangtx  15343  rpmulcxp  15414  rpcxpmul2  15418  binom4  15484  lgseisenlem2  15581  2lgsoddprmlem2  15616  2sqlem4  15628  2sqlem8  15633