Theorem adddid 8171

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 8131	. 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 6001   CCcc 7997   + caddc 8002   x. cmul 8004

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 8103

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

This theorem is referenced by:  subdi  8531  mulreim  8751  apadd1  8755  conjmulap  8876  cju  9108  flhalf  10522  modqcyc  10581  addmodlteq  10620  binom2  10873  binom3  10879  sqoddm1div8  10915  bcpasc  10988  remim  11371  mulreap  11375  readd  11380  remullem  11382  imadd  11388  cjadd  11395  bdtrilem  11750  fsummulc2  11959  binomlem  11994  tanval3ap  12225  sinadd  12247  tanaddap  12250  bezoutlemnewy  12517  dvdsmulgcd  12546  lcmgcdlem  12599  pythagtriplem1  12788  pcaddlem  12862  mul4sqlem  12916  tangtx  15512  rpmulcxp  15583  rpcxpmul2  15587  binom4  15653  lgseisenlem2  15750  2lgsoddprmlem2  15785  2sqlem4  15797  2sqlem8  15802