Theorem adddid 10064

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

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10003

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  addid1  10216  cnegex  10217  addcom  10222  addcomd  10238  subdi  10463  conjmul  10742  cju  11016  flhalf  12631  modcyc  12705  addmodlteq  12745  binom3  12985  sqoddm1div8  13028  bcpasc  13108  hashf1lem2  13240  remim  13857  mulre  13861  readd  13866  remullem  13868  imadd  13874  cjadd  13881  sqreulem  14099  iseraltlem2  14413  o1fsum  14545  binomlem  14561  climcndslem2  14582  binomfallfaclem2  14771  bpoly4  14790  tanval3  14864  sinadd  14894  tanadd  14897  dvdsmulgcd  15274  lcmgcdlem  15319  pythagtriplem1  15521  pcaddlem  15592  prmreclem4  15623  prmreclem6  15625  mul4sqlem  15657  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  nn0srg  19816  rge0srg  19817  icopnfcnv  22741  pcoass  22824  cphipval2  23040  minveclem2  23197  pjthlem1  23208  ovolunlem1a  23264  ovolscalem1  23281  itgcnlem  23556  itgadd  23591  itgmulc2  23600  itgsplit  23602  aaliou3lem2  24098  abelthlem7  24192  tangtx  24257  efgh  24287  tanarg  24365  logcnlem4  24391  mulcxp  24431  cxpmul2  24435  heron  24565  quad2  24566  dcubic1lem  24570  dcubic2  24571  mcubic  24574  binom4  24577  quart1  24583  atanlogsublem  24642  2efiatan  24645  lgamgulmlem3  24757  basellem2  24808  basellem3  24809  basellem8  24814  chtub  24937  bposlem9  25017  lgseisenlem2  25101  2lgsoddprmlem2  25134  2sqlem4  25146  2sqlem8  25151  dchrisumlem1  25178  dchrvmasum2if  25186  dchrisum0re  25202  mulog2sumlem1  25223  selberglem1  25234  selberglem2  25235  selberg  25237  selberg2  25240  chpdifbndlem1  25242  selberg3lem1  25246  selberg4  25250  pntsval2  25265  pntibndlem2  25280  pntlemr  25291  pntlemf  25294  pntlemo  25296  ostth2lem2  25323  ostth2lem3  25324  brbtwn2  25785  axsegconlem9  25805  axpasch  25821  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  finsumvtxdg2ssteplem4  26444  ipasslem2  27687  minvecolem2  27731  pjhthlem1  28250  circlemeth  30718  subfacval2  31169  subfaclim  31170  faclimlem1  31629  itgaddnc  33470  itgmulc2nc  33478  dvasin  33496  pellexlem6  37398  pell1234qrmulcl  37419  rmxyadd  37486  jm2.25  37566  relexpmulnn  38001  binomcxplemnotnn0  38555  sumnnodd  39862  dvnmul  40158  stoweidlem13  40230  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem1  40291  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  fourierdlem83  40406  hoidmvlelem2  40810  hspmbllem1  40840  smfmullem1  40998  deccarry  41321  fmtnorec4  41461  mod42tp1mod8  41519  lighneallem3  41524  opoeALTV  41594  opeoALTV  41595  2zlidl  41934  2zrngamgm  41939  altgsumbcALT  42131