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

Theorem mulid2i 9896
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 9891 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2ax-mp 5 1 (1 · 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  (class class class)co 6524  cc 9787  1c1 9790   · cmul 9794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-mulcl 9851  ax-mulcom 9853  ax-mulass 9855  ax-distr 9856  ax-1rid 9859  ax-cnre 9862
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527
This theorem is referenced by:  00id  10059  halfpm6th  11097  div4p1lem1div2  11131  3halfnz  11285  crreczi  12803  sq10  12862  fac2  12880  hashxplem  13029  bpoly1  14564  bpoly2  14570  bpoly3  14571  bpoly4  14572  efival  14664  ef01bndlem  14696  3dvdsdec  14835  3dvdsdecOLD  14836  3dvds2dec  14837  3dvds2decOLD  14838  odd2np1lem  14845  m1expo  14873  m1exp1  14874  nno  14879  divalglem5  14901  gcdaddmlem  15026  prmo2  15525  dec5nprm  15551  2exp8  15577  13prm  15604  23prm  15607  37prm  15609  43prm  15610  83prm  15611  139prm  15612  163prm  15613  317prm  15614  631prm  15615  1259lem2  15620  1259lem3  15621  1259lem4  15622  1259lem5  15623  2503lem1  15625  2503lem2  15626  2503lem3  15627  2503prm  15628  4001lem1  15629  4001lem2  15630  4001lem3  15631  4001lem4  15632  cnmsgnsubg  19684  sin2pim  23955  cos2pim  23956  sincosq3sgn  23970  sincosq4sgn  23971  tangtx  23975  sincosq1eq  23982  sincos4thpi  23983  sincos6thpi  23985  pige3  23987  abssinper  23988  ang180lem2  24254  ang180lem3  24255  1cubr  24283  asin1  24335  dvatan  24376  log2cnv  24385  log2ublem3  24389  log2ub  24390  logfacbnd3  24662  bclbnd  24719  bpos1  24722  bposlem8  24730  lgsdilem  24763  lgsdir2lem1  24764  lgsdir2lem4  24767  lgsdir2lem5  24768  lgsdir2  24769  lgsdir  24771  2lgsoddprmlem3c  24851  dchrisum0flblem1  24911  rpvmasum2  24915  log2sumbnd  24947  ax5seglem7  25530  ex-fl  26459  ipasslem10  26881  hisubcomi  27148  normlem1  27154  normlem9  27162  norm-ii-i  27181  normsubi  27185  polid2i  27201  lnophmlem2  28063  lnfn0i  28088  nmopcoi  28141  unierri  28150  addltmulALT  28492  sgnmul  29734  problem4  30619  quad3  30621  cnndvlem1  31501  sin2h  32369  poimirlem26  32405  cntotbnd  32565  areaquad  36621  coskpi2  38550  stoweidlem13  38707  wallispilem2  38760  wallispilem4  38762  wallispi2lem1  38765  dirkerper  38790  dirkertrigeqlem1  38792  dirkercncflem1  38797  sqwvfoura  38922  sqwvfourb  38923  fourierswlem  38924  fouriersw  38925  257prm  39813  fmtnofac1  39822  fmtno4prmfac  39824  fmtno4nprmfac193  39826  fmtno5faclem1  39831  fmtno5faclem2  39832  139prmALT  39851  127prm  39855  tgoldbach  40034  tgoldbachOLD  40041
  Copyright terms: Public domain W3C validator