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

Theorem mulid2i 10028
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 10023 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2ax-mp 5 1 (1 · 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wcel 1988  (class class class)co 6635  cc 9919  1c1 9922   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-mulcl 9983  ax-mulcom 9985  ax-mulass 9987  ax-distr 9988  ax-1rid 9991  ax-cnre 9994
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638
This theorem is referenced by:  00id  10196  halfpm6th  11238  div4p1lem1div2  11272  3halfnz  11441  crreczi  12972  sq10  13031  fac2  13049  hashxplem  13203  bpoly1  14763  bpoly2  14769  bpoly3  14770  bpoly4  14771  efival  14863  ef01bndlem  14895  3dvdsdec  15035  3dvdsdecOLD  15036  3dvds2dec  15037  3dvds2decOLD  15038  odd2np1lem  15045  m1expo  15073  m1exp1  15074  nno  15079  divalglem5  15101  gcdaddmlem  15226  prmo2  15725  dec5nprm  15751  2exp8  15777  13prm  15804  23prm  15807  37prm  15809  43prm  15810  83prm  15811  139prm  15812  163prm  15813  317prm  15814  631prm  15815  1259lem2  15820  1259lem3  15821  1259lem4  15822  1259lem5  15823  2503lem1  15825  2503lem2  15826  2503lem3  15827  2503prm  15828  4001lem1  15829  4001lem2  15830  4001lem3  15831  4001lem4  15832  cnmsgnsubg  19904  sin2pim  24218  cos2pim  24219  sincosq3sgn  24233  sincosq4sgn  24234  tangtx  24238  sincosq1eq  24245  sincos4thpi  24246  sincos6thpi  24248  pige3  24250  abssinper  24251  ang180lem2  24521  ang180lem3  24522  1cubr  24550  asin1  24602  dvatan  24643  log2cnv  24652  log2ublem3  24656  log2ub  24657  logfacbnd3  24929  bclbnd  24986  bpos1  24989  bposlem8  24997  lgsdilem  25030  lgsdir2lem1  25031  lgsdir2lem4  25034  lgsdir2lem5  25035  lgsdir2  25036  lgsdir  25038  2lgsoddprmlem3c  25118  dchrisum0flblem1  25178  rpvmasum2  25182  log2sumbnd  25214  ax5seglem7  25796  ex-fl  27274  ipasslem10  27664  hisubcomi  27931  normlem1  27937  normlem9  27945  norm-ii-i  27964  normsubi  27968  polid2i  27984  lnophmlem2  28846  lnfn0i  28871  nmopcoi  28924  unierri  28933  addltmulALT  29275  dpmul4  29596  sgnmul  30578  logdivsqrle  30702  hgt750lem  30703  hgt750lem2  30704  problem4  31536  quad3  31538  cnndvlem1  32503  sin2h  33370  poimirlem26  33406  cntotbnd  33566  areaquad  37621  coskpi2  39840  stoweidlem13  39993  wallispilem2  40046  wallispilem4  40048  wallispi2lem1  40051  dirkerper  40076  dirkertrigeqlem1  40078  dirkercncflem1  40083  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  257prm  41238  fmtnofac1  41247  fmtno4prmfac  41249  fmtno4nprmfac193  41251  fmtno5faclem1  41256  fmtno5faclem2  41257  139prmALT  41276  127prm  41280  tgoldbach  41470  tgoldbachOLD  41477
  Copyright terms: Public domain W3C validator