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

Theorem mulid1i 9619
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
axi.1
Assertion
Ref Expression
mulid1i

Proof of Theorem mulid1i
StepHypRef Expression
1 axi.1 . 2
2 mulid1 9614 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511  1c1 9514   cmul 9518
This theorem is referenced by:  addid1  9781  0lt1  10100  muleqadd  10218  1t1e1  10708  2t1e2  10709  3t1e3  10711  halfpm6th  10785  numltc  11024  numsucc  11030  dec10p  11033  numadd  11038  numaddc  11039  4t3lem  11075  nn0opthlem1  12348  faclbnd4lem1  12371  rei  12989  imi  12990  cji  12992  sqrtm1  13109  0.999...  13690  efival  13887  ef01bndlem  13919  decsplit0b  14566  2exp8  14574  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001prm  14627  cnmsgnsubg  18613  mdetralt  19110  dveflem  22380  dvsincos  22382  efhalfpi  22864  pige3  22910  cosne0  22917  efif1olem4  22932  logf1o2  23031  asin1  23225  dvatan  23266  log2ublem3  23279  log2ub  23280  birthday  23284  basellem9  23362  ppiub  23479  chtub  23487  bposlem8  23566  lgsdir2  23603  mulog2sumlem2  23720  pntlemb  23782  avril1  25171  ipidsq  25623  nmopadjlem  27008  nmopcoadji  27020  unierri  27023  sgnmul  28481  signswch  28518  circum  29040  dvasin  30103  3lcm2e6  31219  wallispi  31852  wallispi2lem2  31854  stirlinglem1  31856  dirkertrigeqlem3  31882  inductionexd  37967
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-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586
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-ral 2812  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