MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid2i Structured version   Visualization version   GIF version

Theorem mulid2i 11094
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
axi.1 ๐ด โˆˆ โ„‚
Assertion
Ref Expression
mulid2i (1 ยท ๐ด) = ๐ด

Proof of Theorem mulid2i
StepHypRef Expression
1 axi.1 . 2 ๐ด โˆˆ โ„‚
2 mulid2 11088 . 2 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = ๐ด)
31, 2ax-mp 5 1 (1 ยท ๐ด) = ๐ด
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7350  โ„‚cc 10983  1c1 10986   ยท cmul 10990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-mulcl 11047  ax-mulcom 11049  ax-mulass 11051  ax-distr 11052  ax-1rid 11055  ax-cnre 11058
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353
This theorem is referenced by:  00id  11264  halfpm6th  12308  div4p1lem1div2  12342  3halfnz  12513  crreczi  14057  fac2  14107  hashxplem  14261  bpoly1  15869  bpoly2  15875  bpoly3  15876  bpoly4  15877  efival  15969  ef01bndlem  16001  3dvdsdec  16149  3dvds2dec  16150  odd2np1lem  16157  m1expo  16192  m1exp1  16193  nno  16199  divalglem5  16214  gcdaddmlem  16339  prmo2  16847  dec5nprm  16873  2exp8  16896  13prm  16923  23prm  16926  37prm  16928  43prm  16929  83prm  16930  139prm  16931  163prm  16932  317prm  16933  631prm  16934  1259lem2  16939  1259lem3  16940  1259lem4  16941  1259lem5  16942  2503lem1  16944  2503lem2  16945  2503lem3  16946  2503prm  16947  4001lem1  16948  4001lem2  16949  4001lem3  16950  4001lem4  16951  cnmsgnsubg  20904  sin2pim  25764  cos2pim  25765  sincosq3sgn  25779  sincosq4sgn  25780  tangtx  25784  sincosq1eq  25791  sincos4thpi  25792  sincos6thpi  25794  pige3ALT  25798  abssinper  25799  ang180lem2  26082  ang180lem3  26083  1cubr  26114  asin1  26166  dvatan  26207  log2cnv  26216  log2ublem3  26220  log2ub  26221  logfacbnd3  26493  bclbnd  26550  bpos1  26553  bposlem8  26561  lgsdilem  26594  lgsdir2lem1  26595  lgsdir2lem4  26598  lgsdir2lem5  26599  lgsdir2  26600  lgsdir  26602  2lgsoddprmlem3c  26682  dchrisum0flblem1  26778  rpvmasum2  26782  log2sumbnd  26814  ax5seglem7  27670  ex-fl  29177  ipasslem10  29567  hisubcomi  29832  normlem1  29838  normlem9  29846  norm-ii-i  29865  normsubi  29869  polid2i  29885  lnophmlem2  30745  lnfn0i  30770  nmopcoi  30823  unierri  30832  addltmulALT  31174  dpmul4  31552  sgnmul  32903  logdivsqrle  33024  hgt750lem  33025  hgt750lem2  33026  problem4  34019  quad3  34021  cnndvlem1  34886  sin2h  35954  poimirlem26  35990  cntotbnd  36141  60gcd6e6  40347  12lcm5e60  40351  60lcm7e420  40353  3lexlogpow5ineq1  40397  3lexlogpow5ineq5  40403  sqdeccom12  40650  ex-decpmul  40653  areaquad  41384  resqrtvalex  41648  imsqrtvalex  41649  coskpi2  43829  stoweidlem13  43976  wallispilem2  44029  wallispilem4  44031  wallispi2lem1  44034  dirkerper  44059  dirkertrigeqlem1  44061  dirkercncflem1  44066  sqwvfoura  44191  sqwvfourb  44192  fourierswlem  44193  fouriersw  44194  257prm  45471  fmtnofac1  45480  fmtno4prmfac  45482  fmtno4nprmfac193  45484  fmtno5faclem1  45489  fmtno5faclem2  45490  139prmALT  45506  127prm  45509  11t31e341  45642  2exp340mod341  45643  nfermltl8rev  45652  tgoldbach  45727
  Copyright terms: Public domain W3C validator