Theorem adddid 8194

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8020   + caddc 8025   x. cmul 8027

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 8126

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

This theorem is referenced by:  subdi  8554  mulreim  8774  apadd1  8778  conjmulap  8899  cju  9131  flhalf  10552  modqcyc  10611  addmodlteq  10650  binom2  10903  binom3  10909  sqoddm1div8  10945  bcpasc  11018  remim  11411  mulreap  11415  readd  11420  remullem  11422  imadd  11428  cjadd  11435  bdtrilem  11790  fsummulc2  11999  binomlem  12034  tanval3ap  12265  sinadd  12287  tanaddap  12290  bezoutlemnewy  12557  dvdsmulgcd  12586  lcmgcdlem  12639  pythagtriplem1  12828  pcaddlem  12902  mul4sqlem  12956  tangtx  15552  rpmulcxp  15623  rpcxpmul2  15627  binom4  15693  lgseisenlem2  15790  2lgsoddprmlem2  15825  2sqlem4  15837  2sqlem8  15842