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

Theorem mulid2i 11093
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 11087 . 2 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = ๐ด)
31, 2ax-mp 5 1 (1 ยท ๐ด) = ๐ด
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541   โˆˆ wcel 2106  (class class class)co 7349  โ„‚cc 10982  1c1 10985   ยท cmul 10989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-mulcl 11046  ax-mulcom 11048  ax-mulass 11050  ax-distr 11051  ax-1rid 11054  ax-cnre 11057
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6443  df-fv 6499  df-ov 7352
This theorem is referenced by:  00id  11263  halfpm6th  12307  div4p1lem1div2  12341  3halfnz  12512  crreczi  14056  fac2  14106  hashxplem  14260  bpoly1  15868  bpoly2  15874  bpoly3  15875  bpoly4  15876  efival  15968  ef01bndlem  16000  3dvdsdec  16148  3dvds2dec  16149  odd2np1lem  16156  m1expo  16191  m1exp1  16192  nno  16198  divalglem5  16213  gcdaddmlem  16338  prmo2  16846  dec5nprm  16872  2exp8  16895  13prm  16922  23prm  16925  37prm  16927  43prm  16928  83prm  16929  139prm  16930  163prm  16931  317prm  16932  631prm  16933  1259lem2  16938  1259lem3  16939  1259lem4  16940  1259lem5  16941  2503lem1  16943  2503lem2  16944  2503lem3  16945  2503prm  16946  4001lem1  16947  4001lem2  16948  4001lem3  16949  4001lem4  16950  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  27682  ex-fl  29189  ipasslem10  29579  hisubcomi  29844  normlem1  29850  normlem9  29858  norm-ii-i  29877  normsubi  29881  polid2i  29897  lnophmlem2  30757  lnfn0i  30782  nmopcoi  30835  unierri  30844  addltmulALT  31186  dpmul4  31564  sgnmul  32915  logdivsqrle  33036  hgt750lem  33037  hgt750lem2  33038  problem4  34031  quad3  34033  cnndvlem1  34895  sin2h  35963  poimirlem26  35999  cntotbnd  36150  60gcd6e6  40356  12lcm5e60  40360  60lcm7e420  40362  3lexlogpow5ineq1  40406  3lexlogpow5ineq5  40412  sqdeccom12  40671  ex-decpmul  40674  areaquad  41415  resqrtvalex  41679  imsqrtvalex  41680  coskpi2  43860  stoweidlem13  44007  wallispilem2  44060  wallispilem4  44062  wallispi2lem1  44065  dirkerper  44090  dirkertrigeqlem1  44092  dirkercncflem1  44097  sqwvfoura  44222  sqwvfourb  44223  fourierswlem  44224  fouriersw  44225  257prm  45502  fmtnofac1  45511  fmtno4prmfac  45513  fmtno4nprmfac193  45515  fmtno5faclem1  45520  fmtno5faclem2  45521  139prmALT  45537  127prm  45540  11t31e341  45673  2exp340mod341  45674  nfermltl8rev  45683  tgoldbach  45758
  Copyright terms: Public domain W3C validator