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

Theorem mulid2i 10635
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
axi.1 𝐴 ∈ ℂ
Assertion
Ref Expression
mulid2i (1 · 𝐴) = 𝐴

Proof of Theorem mulid2i
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 mulid2 10629 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2ax-mp 5 1 (1 · 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2114  (class class class)co 7140  cc 10524  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143
This theorem is referenced by:  00id  10804  halfpm6th  11846  div4p1lem1div2  11880  3halfnz  12049  crreczi  13585  fac2  13635  hashxplem  13790  bpoly1  15396  bpoly2  15402  bpoly3  15403  bpoly4  15404  efival  15496  ef01bndlem  15528  3dvdsdec  15672  3dvds2dec  15673  odd2np1lem  15680  m1expo  15715  m1exp1  15716  nno  15722  divalglem5  15737  gcdaddmlem  15861  prmo2  16365  dec5nprm  16391  2exp8  16414  13prm  16440  23prm  16443  37prm  16445  43prm  16446  83prm  16447  139prm  16448  163prm  16449  317prm  16450  631prm  16451  1259lem2  16456  1259lem3  16457  1259lem4  16458  1259lem5  16459  2503lem1  16461  2503lem2  16462  2503lem3  16463  2503prm  16464  4001lem1  16465  4001lem2  16466  4001lem3  16467  4001lem4  16468  cnmsgnsubg  20264  sin2pim  25076  cos2pim  25077  sincosq3sgn  25091  sincosq4sgn  25092  tangtx  25096  sincosq1eq  25103  sincos4thpi  25104  sincos6thpi  25106  pige3ALT  25110  abssinper  25111  ang180lem2  25394  ang180lem3  25395  1cubr  25426  asin1  25478  dvatan  25519  log2cnv  25528  log2ublem3  25532  log2ub  25533  logfacbnd3  25805  bclbnd  25862  bpos1  25865  bposlem8  25873  lgsdilem  25906  lgsdir2lem1  25907  lgsdir2lem4  25910  lgsdir2lem5  25911  lgsdir2  25912  lgsdir  25914  2lgsoddprmlem3c  25994  dchrisum0flblem1  26090  rpvmasum2  26094  log2sumbnd  26126  ax5seglem7  26727  ex-fl  28230  ipasslem10  28620  hisubcomi  28885  normlem1  28891  normlem9  28899  norm-ii-i  28918  normsubi  28922  polid2i  28938  lnophmlem2  29798  lnfn0i  29823  nmopcoi  29876  unierri  29885  addltmulALT  30227  dpmul4  30600  sgnmul  31874  logdivsqrle  31995  hgt750lem  31996  hgt750lem2  31997  problem4  32985  quad3  32987  cnndvlem1  33950  sin2h  35009  poimirlem26  35045  cntotbnd  35196  60gcd6e6  39257  12lcm5e60  39261  60lcm7e420  39263  sqdeccom12  39431  ex-decpmul  39434  areaquad  40100  resqrtvalex  40279  imsqrtvalex  40280  coskpi2  42451  stoweidlem13  42598  wallispilem2  42651  wallispilem4  42653  wallispi2lem1  42656  dirkerper  42681  dirkertrigeqlem1  42683  dirkercncflem1  42688  sqwvfoura  42813  sqwvfourb  42814  fourierswlem  42815  fouriersw  42816  257prm  44021  fmtnofac1  44030  fmtno4prmfac  44032  fmtno4nprmfac193  44034  fmtno5faclem1  44039  fmtno5faclem2  44040  139prmALT  44056  127prm  44059  11t31e341  44193  2exp340mod341  44194  nfermltl8rev  44203  tgoldbach  44278
  Copyright terms: Public domain W3C validator