Theorem adddid 8046

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5919   CCcc 7872   + caddc 7877   x. cmul 7879

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 7978

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

This theorem is referenced by:  subdi  8406  mulreim  8625  apadd1  8629  conjmulap  8750  cju  8982  flhalf  10374  modqcyc  10433  addmodlteq  10472  binom2  10725  binom3  10731  sqoddm1div8  10767  bcpasc  10840  remim  11007  mulreap  11011  readd  11016  remullem  11018  imadd  11024  cjadd  11031  bdtrilem  11385  fsummulc2  11594  binomlem  11629  tanval3ap  11860  sinadd  11882  tanaddap  11885  bezoutlemnewy  12136  dvdsmulgcd  12165  lcmgcdlem  12218  pythagtriplem1  12406  pcaddlem  12480  mul4sqlem  12534  tangtx  15014  rpmulcxp  15085  binom4  15152  lgseisenlem2  15228  2lgsoddprmlem2  15263  2sqlem4  15275  2sqlem8  15280