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

Theorem mulid2i 9026
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 9022 . 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 1649    e. wcel 1717  (class class class)co 6020   CCcc 8921   1c1 8924    x. cmul 8928
This theorem is referenced by:  00id  9173  halfpm6th  10124  crreczi  11431  fac2  11499  hashxplem  11623  efival  12680  ef01bndlem  12712  odd2np1lem  12834  divalglem5  12844  gcdaddmlem  12955  dec5nprm  13329  2exp6  13349  2exp8  13350  13prm  13365  23prm  13368  37prm  13370  43prm  13371  83prm  13372  139prm  13373  163prm  13374  317prm  13375  631prm  13376  1259lem2  13378  1259lem3  13379  1259lem4  13380  1259lem5  13381  2503lem1  13383  2503lem2  13384  2503lem3  13385  2503prm  13386  4001lem1  13387  4001lem2  13388  4001lem3  13389  4001lem4  13390  sin2pim  20260  cos2pim  20261  sincosq3sgn  20275  sincosq4sgn  20276  tangtx  20280  sincosq1eq  20287  sincos4thpi  20288  sincos6thpi  20290  pige3  20292  abssinper  20293  ang180lem2  20519  ang180lem3  20520  1cubr  20549  asin1  20601  dvatan  20642  log2cnv  20651  log2ublem3  20655  log2ub  20656  logfacbnd3  20874  bclbnd  20931  bpos1  20934  bposlem8  20942  lgsdilem  20973  lgsdir2lem1  20974  lgsdir2lem4  20977  lgsdir2lem5  20978  lgsdir2  20979  lgsdir  20981  dchrisum0flblem1  21069  rpvmasum2  21073  log2sumbnd  21105  ex-fl  21603  ipasslem10  22188  hisubcomi  22454  normlem1  22460  normlem9  22468  norm-ii-i  22487  normsubi  22491  polid2i  22507  lnophmlem2  23368  lnfn0i  23393  nmopcoi  23446  unierri  23455  addltmulALT  23797  ax5seglem7  25588  bpoly1  25811  bpoly2  25817  bpoly3  25818  bpoly4  25819  cntotbnd  26196  cnmsgnsubg  27103  stoweidlem13  27430  wallispilem2  27483  wallispilem4  27485  wallispi2lem1  27488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-mulcl 8985  ax-mulcom 8987  ax-mulass 8989  ax-distr 8990  ax-1rid 8993  ax-cnre 8996
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023
  Copyright terms: Public domain W3C validator