MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adddird Unicode version

Theorem adddird 9642
Description: Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1
addcld.2
addassd.3
Assertion
Ref Expression
adddird

Proof of Theorem adddird
StepHypRef Expression
1 addcld.1 . 2
2 addcld.2 . 2
3 addassd.3 . 2
4 adddir 9608 . 2
51, 2, 3, 4syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516   cmul 9518
This theorem is referenced by:  1p1times  9772  recextlem1  10204  divdir  10255  ltdifltdiv  11966  modvalp1  12014  subsq  12275  subsq2  12276  binom3  12287  discr1  12302  cshweqrep  12789  remullem  12961  sqrlem7  13082  binomlem  13641  arisum  13671  smumullem  14142  bezoutlem3  14178  bezoutlem4  14179  pcexp  14383  mul4sqlem  14471  vdwapun  14492  mulgnnass  16170  cnfldmulg  18450  nn0srg  18486  rge0srg  18487  nmotri  21246  blcvx  21303  itg1addlem5  22107  mbfi1fseqlem4  22125  itgconst  22225  itgmulc2  22240  dvexp  22356  dvcvx  22421  plyaddlem1  22610  dgrcolem1  22670  abelthlem2  22827  abelthlem7  22833  tangtx  22898  cxpadd  23060  dcubic  23177  binom4  23181  dquartlem2  23183  dquart  23184  quart1lem  23186  quart1  23187  cvxcl  23314  scvxcvx  23315  basellem9  23362  bposlem9  23567  lgsquad2lem1  23633  2sqlem4  23642  2sqblem  23652  dchrisumlem2  23675  dchrisum0lem1  23701  mudivsum  23715  chpdifbndlem1  23738  pntrlog2bndlem2  23763  pntlemr  23787  pntlemk  23791  ostth2lem2  23819  brbtwn2  24208  ax5seglem3  24234  ax5seglem5  24236  axbtwnid  24242  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  ex-ind-dvds  25170  smcnlem  25607  subfacp1lem6  28629  subfacval2  28631  subfaclim  28632  cvxscon  28688  rescon  28691  binomfallfaclem2  29162  itg2addnclem3  30068  itgmulc2nc  30083  rrnequiv  30331  jm2.19lem3  30933  jm2.25  30941  jm3.1lem2  30960  binomcxplemwb  31253  binomcxplemnotnn0  31261  adddirp1d  31486  fperiodmullem  31503  coskpi2  31666  cosknegpi  31669  dvnmul  31740  stoweidlem11  31793  stoweidlem13  31795  stirlinglem1  31856  stirlinglem4  31859  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  dirkercncflem2  31886  fourierdlem41  31930  fourierdlem42  31931  fourierdlem64  31953  fourierswlem  32013  sigaraf  32070  joinlmuladdmuld  33187  sineq0ALT  33737  inductionexd  37967  int-leftdistd  38000  int-rightdistd  38001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-addcl 9573  ax-mulcom 9577  ax-distr 9580
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator