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

Theorem mulid2i 9387
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 9382 . 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 1369    e. wcel 1756  (class class class)co 6089   CCcc 9278   1c1 9281    x. cmul 9285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-mulcl 9342  ax-mulcom 9344  ax-mulass 9346  ax-distr 9347  ax-1rid 9350  ax-cnre 9353
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-br 4291  df-iota 5379  df-fv 5424  df-ov 6092
This theorem is referenced by:  00id  9542  halfpm6th  10544  crreczi  11987  fac2  12055  hashxplem  12193  efival  13434  ef01bndlem  13466  odd2np1lem  13589  divalglem5  13599  gcdaddmlem  13710  dec5nprm  14093  2exp6  14113  2exp8  14114  13prm  14141  23prm  14144  37prm  14146  43prm  14147  83prm  14148  139prm  14149  163prm  14150  317prm  14151  631prm  14152  1259lem2  14154  1259lem3  14155  1259lem4  14156  1259lem5  14157  2503lem1  14159  2503lem2  14160  2503lem3  14161  2503prm  14162  4001lem1  14163  4001lem2  14164  4001lem3  14165  4001lem4  14166  cnmsgnsubg  18005  sin2pim  21945  cos2pim  21946  sincosq3sgn  21960  sincosq4sgn  21961  tangtx  21965  sincosq1eq  21972  sincos4thpi  21973  sincos6thpi  21975  pige3  21977  abssinper  21978  ang180lem2  22204  ang180lem3  22205  1cubr  22235  asin1  22287  dvatan  22328  log2cnv  22337  log2ublem3  22341  log2ub  22342  logfacbnd3  22560  bclbnd  22617  bpos1  22620  bposlem8  22628  lgsdilem  22659  lgsdir2lem1  22660  lgsdir2lem4  22663  lgsdir2lem5  22664  lgsdir2  22665  lgsdir  22667  dchrisum0flblem1  22755  rpvmasum2  22759  log2sumbnd  22791  ax5seglem7  23179  ex-fl  23652  ipasslem10  24237  hisubcomi  24504  normlem1  24510  normlem9  24518  norm-ii-i  24537  normsubi  24541  polid2i  24557  lnophmlem2  25419  lnfn0i  25444  nmopcoi  25497  unierri  25506  addltmulALT  25848  sgnmul  26923  problem4  27299  quad3  27301  bpoly1  28192  bpoly2  28198  bpoly3  28199  bpoly4  28200  sin2h  28419  cntotbnd  28692  areaquad  29589  stoweidlem13  29805  wallispilem2  29858  wallispilem4  29860  wallispi2lem1  29863
  Copyright terms: Public domain W3C validator