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

Theorem mulid2i 9086
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 9082 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2ax-mp 8 1  |-  ( 1  x.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725  (class class class)co 6074   CCcc 8981   1c1 8984    x. cmul 8988
This theorem is referenced by:  00id  9234  halfpm6th  10185  crreczi  11497  fac2  11565  hashxplem  11689  efival  12746  ef01bndlem  12778  odd2np1lem  12900  divalglem5  12910  gcdaddmlem  13021  dec5nprm  13395  2exp6  13415  2exp8  13416  13prm  13431  23prm  13434  37prm  13436  43prm  13437  83prm  13438  139prm  13439  163prm  13440  317prm  13441  631prm  13442  1259lem2  13444  1259lem3  13445  1259lem4  13446  1259lem5  13447  2503lem1  13449  2503lem2  13450  2503lem3  13451  2503prm  13452  4001lem1  13453  4001lem2  13454  4001lem3  13455  4001lem4  13456  sin2pim  20386  cos2pim  20387  sincosq3sgn  20401  sincosq4sgn  20402  tangtx  20406  sincosq1eq  20413  sincos4thpi  20414  sincos6thpi  20416  pige3  20418  abssinper  20419  ang180lem2  20645  ang180lem3  20646  1cubr  20675  asin1  20727  dvatan  20768  log2cnv  20777  log2ublem3  20781  log2ub  20782  logfacbnd3  21000  bclbnd  21057  bpos1  21060  bposlem8  21068  lgsdilem  21099  lgsdir2lem1  21100  lgsdir2lem4  21103  lgsdir2lem5  21104  lgsdir2  21105  lgsdir  21107  dchrisum0flblem1  21195  rpvmasum2  21199  log2sumbnd  21231  ex-fl  21748  ipasslem10  22333  hisubcomi  22599  normlem1  22605  normlem9  22613  norm-ii-i  22632  normsubi  22636  polid2i  22652  lnophmlem2  23513  lnfn0i  23538  nmopcoi  23591  unierri  23600  addltmulALT  23942  ax5seglem7  25867  bpoly1  26090  bpoly2  26096  bpoly3  26097  bpoly4  26098  cntotbnd  26497  cnmsgnsubg  27403  stoweidlem13  27730  wallispilem2  27783  wallispilem4  27785  wallispi2lem1  27788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-resscn 9040  ax-1cn 9041  ax-icn 9042  ax-addcl 9043  ax-mulcl 9045  ax-mulcom 9047  ax-mulass 9049  ax-distr 9050  ax-1rid 9053  ax-cnre 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-iota 5411  df-fv 5455  df-ov 6077
  Copyright terms: Public domain W3C validator