Theorem adddid 8182

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 8142	. 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 6007   CCcc 8008   + caddc 8013   x. cmul 8015

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 8114

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

This theorem is referenced by:  subdi  8542  mulreim  8762  apadd1  8766  conjmulap  8887  cju  9119  flhalf  10534  modqcyc  10593  addmodlteq  10632  binom2  10885  binom3  10891  sqoddm1div8  10927  bcpasc  11000  remim  11387  mulreap  11391  readd  11396  remullem  11398  imadd  11404  cjadd  11411  bdtrilem  11766  fsummulc2  11975  binomlem  12010  tanval3ap  12241  sinadd  12263  tanaddap  12266  bezoutlemnewy  12533  dvdsmulgcd  12562  lcmgcdlem  12615  pythagtriplem1  12804  pcaddlem  12878  mul4sqlem  12932  tangtx  15528  rpmulcxp  15599  rpcxpmul2  15603  binom4  15669  lgseisenlem2  15766  2lgsoddprmlem2  15801  2sqlem4  15813  2sqlem8  15818