Theorem adddird 10065

Description: Distributive law (right-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
adddird	|- ( ph -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )

Proof of Theorem adddird

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		adddir 10031	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
5	1, 2, 3, 4	syl3anc 1326	1 |- ( ph -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B 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-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-addcl 9996  ax-mulcom 10000  ax-distr 10003

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  adddirp1d  10066  joinlmuladdmuld  10067  recextlem1  10657  divdir  10710  ltdifltdiv  12635  subsq  12972  subsq2  12973  binom3  12985  discr1  13000  cshweqrep  13567  remullem  13868  sqrlem7  13989  binomlem  14561  arisum  14592  binomfallfaclem2  14771  pwp1fsum  15114  smumullem  15214  bezoutlem3  15258  bezoutlem4  15259  pcexp  15564  mul4sqlem  15657  vdwapun  15678  mulgnnass  17576  mulgnnassOLD  17577  cnfldmulg  19778  nn0srg  19816  rge0srg  19817  nmotri  22543  blcvx  22601  cphipval2  23040  itg1addlem5  23467  mbfi1fseqlem4  23485  itgconst  23585  itgmulc2  23600  dvexp  23716  dvcvx  23783  plyaddlem1  23969  dgrcolem1  24029  abelthlem2  24186  abelthlem7  24192  tangtx  24257  cxpadd  24425  dcubic  24573  binom4  24577  dquartlem2  24579  dquart  24580  quart1lem  24582  quart1  24583  cvxcl  24711  scvxcvx  24712  basellem9  24815  bposlem9  25017  lgsquad2lem1  25109  2sqlem4  25146  2sqblem  25156  dchrisumlem2  25179  dchrisum0lem1  25205  mudivsum  25219  chpdifbndlem1  25242  pntrlog2bndlem2  25267  pntlemr  25291  pntlemk  25295  ostth2lem2  25323  brbtwn2  25785  ax5seglem3  25811  ax5seglem5  25813  axbtwnid  25819  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  ex-ind-dvds  27318  smcnlem  27552  circlemeth  30718  hgt750lemd  30726  logdivsqrle  30728  subfacp1lem6  31167  subfacval2  31169  subfaclim  31170  cvxsconn  31225  resconn  31228  fwddifnp1  32272  itg2addnclem3  33463  itgmulc2nc  33478  rrnequiv  33634  jm2.19lem3  37558  jm2.25  37566  jm3.1lem2  37585  inductionexd  38453  int-leftdistd  38482  binomcxplemwb  38547  binomcxplemnotnn0  38555  sineq0ALT  39173  fperiodmullem  39517  xralrple2  39570  coskpi2  40077  cosknegpi  40080  dvnmul  40158  stoweidlem11  40228  stoweidlem13  40230  stirlinglem1  40291  stirlinglem4  40294  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem41  40365  fourierdlem42  40366  fourierdlem64  40387  fourierswlem  40447  hoidmvlelem2  40810  sigaraf  41042  fmtnorec3  41460