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

Theorem mulid2i 10634
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 10628 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2ax-mp 5 1 (1 · 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523  1c1 10526   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  00id  10803  halfpm6th  11846  div4p1lem1div2  11880  3halfnz  12049  crreczi  13577  fac2  13627  hashxplem  13782  bpoly1  15393  bpoly2  15399  bpoly3  15400  bpoly4  15401  efival  15493  ef01bndlem  15525  3dvdsdec  15669  3dvds2dec  15670  odd2np1lem  15677  m1expo  15714  m1exp1  15715  nno  15721  divalglem5  15736  gcdaddmlem  15860  prmo2  16364  dec5nprm  16390  2exp8  16411  13prm  16437  23prm  16440  37prm  16442  43prm  16443  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  cnmsgnsubg  20649  sin2pim  24998  cos2pim  24999  sincosq3sgn  25013  sincosq4sgn  25014  tangtx  25018  sincosq1eq  25025  sincos4thpi  25026  sincos6thpi  25028  pige3ALT  25032  abssinper  25033  ang180lem2  25315  ang180lem3  25316  1cubr  25347  asin1  25399  dvatan  25440  log2cnv  25449  log2ublem3  25453  log2ub  25454  logfacbnd3  25726  bclbnd  25783  bpos1  25786  bposlem8  25794  lgsdilem  25827  lgsdir2lem1  25828  lgsdir2lem4  25831  lgsdir2lem5  25832  lgsdir2  25833  lgsdir  25835  2lgsoddprmlem3c  25915  dchrisum0flblem1  26011  rpvmasum2  26015  log2sumbnd  26047  ax5seglem7  26648  ex-fl  28153  ipasslem10  28543  hisubcomi  28808  normlem1  28814  normlem9  28822  norm-ii-i  28841  normsubi  28845  polid2i  28861  lnophmlem2  29721  lnfn0i  29746  nmopcoi  29799  unierri  29808  addltmulALT  30150  dpmul4  30517  sgnmul  31699  logdivsqrle  31820  hgt750lem  31821  hgt750lem2  31822  problem4  32808  quad3  32810  cnndvlem1  33773  sin2h  34763  poimirlem26  34799  cntotbnd  34955  sqdeccom12  39053  ex-decpmul  39056  areaquad  39701  coskpi2  42023  stoweidlem13  42175  wallispilem2  42228  wallispilem4  42230  wallispi2lem1  42233  dirkerper  42258  dirkertrigeqlem1  42260  dirkercncflem1  42265  sqwvfoura  42390  sqwvfourb  42391  fourierswlem  42392  fouriersw  42393  257prm  43600  fmtnofac1  43609  fmtno4prmfac  43611  fmtno4nprmfac193  43613  fmtno5faclem1  43618  fmtno5faclem2  43619  139prmALT  43636  127prm  43640  11t31e341  43774  2exp340mod341  43775  nfermltl8rev  43784  tgoldbach  43859
  Copyright terms: Public domain W3C validator