Theorem adddid 8263

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8090   + caddc 8095   x. cmul 8097

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 8196

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

This theorem is referenced by:  subdi  8623  mulreim  8843  apadd1  8847  conjmulap  8968  cju  9200  flhalf  10625  modqcyc  10684  addmodlteq  10723  binom2  10976  binom3  10982  sqoddm1div8  11018  bcpasc  11091  remim  11500  mulreap  11504  readd  11509  remullem  11511  imadd  11517  cjadd  11524  bdtrilem  11879  fsummulc2  12089  binomlem  12124  tanval3ap  12355  sinadd  12377  tanaddap  12380  bezoutlemnewy  12647  dvdsmulgcd  12676  lcmgcdlem  12729  pythagtriplem1  12918  pcaddlem  12992  mul4sqlem  13046  tangtx  15649  rpmulcxp  15720  rpcxpmul2  15724  binom4  15790  lgseisenlem2  15890  2lgsoddprmlem2  15925  2sqlem4  15937  2sqlem8  15942