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

Theorem mulid2i 8840
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 8836 . 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 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735   1c1 8738    x. cmul 8742
This theorem is referenced by:  00id  8987  halfpm6th  9936  crreczi  11226  fac2  11294  hashxplem  11385  efival  12432  ef01bndlem  12464  odd2np1lem  12586  divalglem5  12596  gcdaddmlem  12707  dec5nprm  13081  2exp6  13101  2exp8  13102  13prm  13117  23prm  13120  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  sin2pim  19853  cos2pim  19854  sincosq3sgn  19868  sincosq4sgn  19869  tangtx  19873  sincosq1eq  19880  sincos4thpi  19881  sincos6thpi  19883  pige3  19885  abssinper  19886  ang180lem2  20108  ang180lem3  20109  1cubr  20138  asin1  20190  dvatan  20231  log2cnv  20240  log2ublem3  20244  log2ub  20245  logfacbnd3  20462  bclbnd  20519  bpos1  20522  bposlem8  20530  lgsdilem  20561  lgsdir2lem1  20562  lgsdir2lem4  20565  lgsdir2lem5  20566  lgsdir2  20567  lgsdir  20569  dchrisum0flblem1  20657  rpvmasum2  20661  log2sumbnd  20693  ex-fl  20834  ipasslem10  21417  hisubcomi  21683  normlem1  21689  normlem9  21697  norm-ii-i  21716  normsubi  21720  polid2i  21736  lnophmlem2  22597  lnfn0i  22622  nmopcoi  22675  unierri  22684  addltmulALT  23026  ax5seglem7  24563  bpoly1  24786  bpoly2  24792  bpoly3  24793  bpoly4  24794  3timesi  25178  cntotbnd  26520  cnmsgnsubg  27434  wallispilem2  27815  wallispilem4  27817  wallispi2lem1  27820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator