Theorem adddid 8351

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8284

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  subdi  8714  mulreim  8935  apadd1  8939  conjmulap  9062  cju  9294  flhalf  10752  modqcyc  10811  addmodlteq  10850  binom2  11103  binom3  11109  sqoddm1div8  11146  bcpasc  11220  hashf1lem2  11302  remim  11641  mulreap  11645  readd  11650  remullem  11652  imadd  11658  cjadd  11665  bdtrilem  12024  fsummulc2  12234  binomlem  12269  tanval3ap  12500  sinadd  12522  tanaddap  12525  bezoutlemnewy  12792  dvdsmulgcd  12821  lcmgcdlem  12874  pythagtriplem1  13067  pcaddlem  13141  mul4sqlem  13195  tangtx  16031  rpmulcxp  16106  rpcxpmul2  16110  binom4  16180  chtqub  16257  bposlem9  16280  lgseisenlem2  16356  2lgsoddprmlem2  16391  2sqlem4  16403  2sqlem8  16408