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

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulid2 10629	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂ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 2113  ax-9 2121  ax-ext 2770  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 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  00id  10804  halfpm6th  11846  div4p1lem1div2  11880  3halfnz  12049  crreczi  13585  fac2  13635  hashxplem  13790  bpoly1  15397  bpoly2  15403  bpoly3  15404  bpoly4  15405  efival  15497  ef01bndlem  15529  3dvdsdec  15673  3dvds2dec  15674  odd2np1lem  15681  m1expo  15716  m1exp1  15717  nno  15723  divalglem5  15738  gcdaddmlem  15862  prmo2  16366  dec5nprm  16392  2exp8  16415  13prm  16441  23prm  16444  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  cnmsgnsubg  20266  sin2pim  25078  cos2pim  25079  sincosq3sgn  25093  sincosq4sgn  25094  tangtx  25098  sincosq1eq  25105  sincos4thpi  25106  sincos6thpi  25108  pige3ALT  25112  abssinper  25113  ang180lem2  25396  ang180lem3  25397  1cubr  25428  asin1  25480  dvatan  25521  log2cnv  25530  log2ublem3  25534  log2ub  25535  logfacbnd3  25807  bclbnd  25864  bpos1  25867  bposlem8  25875  lgsdilem  25908  lgsdir2lem1  25909  lgsdir2lem4  25912  lgsdir2lem5  25913  lgsdir2  25914  lgsdir  25916  2lgsoddprmlem3c  25996  dchrisum0flblem1  26092  rpvmasum2  26096  log2sumbnd  26128  ax5seglem7  26729  ex-fl  28232  ipasslem10  28622  hisubcomi  28887  normlem1  28893  normlem9  28901  norm-ii-i  28920  normsubi  28924  polid2i  28940  lnophmlem2  29800  lnfn0i  29825  nmopcoi  29878  unierri  29887  addltmulALT  30229  dpmul4  30616  sgnmul  31910  logdivsqrle  32031  hgt750lem  32032  hgt750lem2  32033  problem4  33024  quad3  33026  cnndvlem1  33989  sin2h  35047  poimirlem26  35083  cntotbnd  35234  60gcd6e6  39292  12lcm5e60  39296  60lcm7e420  39298  sqdeccom12  39483  ex-decpmul  39486  areaquad  40166  resqrtvalex  40345  imsqrtvalex  40346  coskpi2  42508  stoweidlem13  42655  wallispilem2  42708  wallispilem4  42710  wallispi2lem1  42713  dirkerper  42738  dirkertrigeqlem1  42740  dirkercncflem1  42745  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  257prm  44078  fmtnofac1  44087  fmtno4prmfac  44089  fmtno4nprmfac193  44091  fmtno5faclem1  44096  fmtno5faclem2  44097  139prmALT  44113  127prm  44116  11t31e341  44250  2exp340mod341  44251  nfermltl8rev  44260  tgoldbach  44335