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

Theorem mulid2i 9599
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 9594 . 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 1379    e. wcel 1767  (class class class)co 6284   CCcc 9490   1c1 9493    x. cmul 9497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-mulcl 9554  ax-mulcom 9556  ax-mulass 9558  ax-distr 9559  ax-1rid 9562  ax-cnre 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287
This theorem is referenced by:  00id  9754  halfpm6th  10760  crreczi  12259  fac2  12327  hashxplem  12457  efival  13748  ef01bndlem  13780  odd2np1lem  13904  divalglem5  13914  gcdaddmlem  14025  dec5nprm  14411  2exp6  14431  2exp8  14432  13prm  14459  23prm  14462  37prm  14464  43prm  14465  83prm  14466  139prm  14467  163prm  14468  317prm  14469  631prm  14470  1259lem2  14472  1259lem3  14473  1259lem4  14474  1259lem5  14475  2503lem1  14477  2503lem2  14478  2503lem3  14479  2503prm  14480  4001lem1  14481  4001lem2  14482  4001lem3  14483  4001lem4  14484  cnmsgnsubg  18408  sin2pim  22639  cos2pim  22640  sincosq3sgn  22654  sincosq4sgn  22655  tangtx  22659  sincosq1eq  22666  sincos4thpi  22667  sincos6thpi  22669  pige3  22671  abssinper  22672  ang180lem2  22898  ang180lem3  22899  1cubr  22929  asin1  22981  dvatan  23022  log2cnv  23031  log2ublem3  23035  log2ub  23036  logfacbnd3  23254  bclbnd  23311  bpos1  23314  bposlem8  23322  lgsdilem  23353  lgsdir2lem1  23354  lgsdir2lem4  23357  lgsdir2lem5  23358  lgsdir2  23359  lgsdir  23361  dchrisum0flblem1  23449  rpvmasum2  23453  log2sumbnd  23485  ax5seglem7  23942  ex-fl  24873  ipasslem10  25458  hisubcomi  25725  normlem1  25731  normlem9  25739  norm-ii-i  25758  normsubi  25762  polid2i  25778  lnophmlem2  26640  lnfn0i  26665  nmopcoi  26718  unierri  26727  addltmulALT  27069  sgnmul  28149  problem4  28525  quad3  28527  bpoly1  29418  bpoly2  29424  bpoly3  29425  bpoly4  29426  sin2h  29650  cntotbnd  29923  areaquad  30817  coskpi2  31230  stoweidlem13  31341  wallispilem2  31394  wallispilem4  31396  wallispi2lem1  31399  dirkertrigeqlem1  31426  sqwvfoura  31557  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560
  Copyright terms: Public domain W3C validator