Theorem adddid 8350

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 8311	. 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 8177   + caddc 8182   x. cmul 8184

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 8283

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

This theorem is used by:  subdi  8712  mulreim  8932  apadd1  8936  conjmulap  9059  cju  9291  flhalf  10737  modqcyc  10796  addmodlteq  10835  binom2  11088  binom3  11094  sqoddm1div8  11131  bcpasc  11204  hashf1lem2  11286  remim  11625  mulreap  11629  readd  11634  remullem  11636  imadd  11642  cjadd  11649  bdtrilem  12005  fsummulc2  12215  binomlem  12250  tanval3ap  12481  sinadd  12503  tanaddap  12506  bezoutlemnewy  12773  dvdsmulgcd  12802  lcmgcdlem  12855  pythagtriplem1  13044  pcaddlem  13118  mul4sqlem  13172  tangtx  15939  rpmulcxp  16011  rpcxpmul2  16015  binom4  16081  lgseisenlem2  16190  2lgsoddprmlem2  16225  2sqlem4  16237  2sqlem8  16242