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

Theorem mulid2i 9588
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
axi.1  |-  A  e.  CC
Assertion
Ref Expression
mulid2i  |-  ( 1  x.  A )  =  A

Proof of Theorem mulid2i
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 mulid2 9583 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2ax-mp 5 1  |-  ( 1  x.  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479   1c1 9482    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-mulcom 9545  ax-mulass 9547  ax-distr 9548  ax-1rid 9551  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  00id  9744  halfpm6th  10756  crreczi  12273  fac2  12341  hashxplem  12475  efival  13969  ef01bndlem  14001  odd2np1lem  14129  divalglem5  14139  gcdaddmlem  14250  dec5nprm  14636  2exp6OLD  14657  2exp8  14658  13prm  14685  23prm  14688  37prm  14690  43prm  14691  83prm  14692  139prm  14693  163prm  14694  317prm  14695  631prm  14696  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  2503lem1  14703  2503lem2  14704  2503lem3  14705  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  cnmsgnsubg  18786  sin2pim  23044  cos2pim  23045  sincosq3sgn  23059  sincosq4sgn  23060  tangtx  23064  sincosq1eq  23071  sincos4thpi  23072  sincos6thpi  23074  pige3  23076  abssinper  23077  ang180lem2  23341  ang180lem3  23342  1cubr  23370  asin1  23422  dvatan  23463  log2cnv  23472  log2ublem3  23476  log2ub  23477  logfacbnd3  23696  bclbnd  23753  bpos1  23756  bposlem8  23764  lgsdilem  23795  lgsdir2lem1  23796  lgsdir2lem4  23799  lgsdir2lem5  23800  lgsdir2  23801  lgsdir  23803  dchrisum0flblem1  23891  rpvmasum2  23895  log2sumbnd  23927  ax5seglem7  24440  ex-fl  25370  ipasslem10  25952  hisubcomi  26219  normlem1  26225  normlem9  26233  norm-ii-i  26252  normsubi  26256  polid2i  26272  lnophmlem2  27134  lnfn0i  27159  nmopcoi  27212  unierri  27221  addltmulALT  27563  sgnmul  28745  problem4  29286  quad3  29288  bpoly1  30041  bpoly2  30047  bpoly3  30048  bpoly4  30049  sin2h  30285  cntotbnd  30532  areaquad  31425  coskpi2  31905  stoweidlem13  32034  wallispilem2  32087  wallispilem4  32089  wallispi2lem1  32092  dirkerper  32117  dirkertrigeqlem1  32119  dirkercncflem1  32124  sqwvfoura  32250  sqwvfourb  32251  fourierswlem  32252  fouriersw  32253  3halfnz  33380  nno  33392
  Copyright terms: Public domain W3C validator