Theorem adddid 8012

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 7973	. 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 2160  (class class class)co 5896   CCcc 7839   + caddc 7844   x. cmul 7846

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 7945

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

This theorem is referenced by:  subdi  8372  mulreim  8591  apadd1  8595  conjmulap  8716  cju  8948  flhalf  10333  modqcyc  10390  addmodlteq  10429  binom2  10663  binom3  10669  sqoddm1div8  10705  bcpasc  10778  remim  10901  mulreap  10905  readd  10910  remullem  10912  imadd  10918  cjadd  10925  bdtrilem  11279  fsummulc2  11488  binomlem  11523  tanval3ap  11754  sinadd  11776  tanaddap  11779  bezoutlemnewy  12029  dvdsmulgcd  12058  lcmgcdlem  12109  pythagtriplem1  12297  pcaddlem  12371  mul4sqlem  12425  tangtx  14719  rpmulcxp  14790  binom4  14857  lgseisenlem2  14912  2lgsoddprmlem2  14915  2sqlem4  14926  2sqlem8  14931