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

Theorem adddii 9627
Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1
axi.2
axi.3
Assertion
Ref Expression
adddii

Proof of Theorem adddii
StepHypRef Expression
1 axi.1 . 2
2 axi.2 . 2
3 axi.3 . 2
4 adddi 9602 . 2
51, 2, 3, 4mp3an 1324 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516   cmul 9518
This theorem is referenced by:  addid1  9781  3t3e9  10713  numltc  11024  numsucc  11030  numma  11035  4t3lem  11075  decbin2  11108  binom2i  12277  faclbnd4lem1  12371  mod2xnegi  14557  decsplit  14569  log2ublem1  23277  log2ublem2  23278  bposlem8  23566  ax5seglem7  24238  ip0i  25740  ip1ilem  25741  ipasslem10  25754  normlem0  26026  polid2i  26074  lnopunilem1  26929  fourierswlem  32013  2t6m3t4e0  32937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9580
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator