Theorem mulid2i 10964

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 10958	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853  1c1 10856   · cmul 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-mulcl 10917  ax-mulcom 10919  ax-mulass 10921  ax-distr 10922  ax-1rid 10925  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  00id  11133  halfpm6th  12177  div4p1lem1div2  12211  3halfnz  12382  crreczi  13924  fac2  13974  hashxplem  14129  bpoly1  15742  bpoly2  15748  bpoly3  15749  bpoly4  15750  efival  15842  ef01bndlem  15874  3dvdsdec  16022  3dvds2dec  16023  odd2np1lem  16030  m1expo  16065  m1exp1  16066  nno  16072  divalglem5  16087  gcdaddmlem  16212  prmo2  16722  dec5nprm  16748  2exp8  16771  13prm  16798  23prm  16801  37prm  16803  43prm  16804  83prm  16805  139prm  16806  163prm  16807  317prm  16808  631prm  16809  1259lem2  16814  1259lem3  16815  1259lem4  16816  1259lem5  16817  2503lem1  16819  2503lem2  16820  2503lem3  16821  2503prm  16822  4001lem1  16823  4001lem2  16824  4001lem3  16825  4001lem4  16826  cnmsgnsubg  20763  sin2pim  25623  cos2pim  25624  sincosq3sgn  25638  sincosq4sgn  25639  tangtx  25643  sincosq1eq  25650  sincos4thpi  25651  sincos6thpi  25653  pige3ALT  25657  abssinper  25658  ang180lem2  25941  ang180lem3  25942  1cubr  25973  asin1  26025  dvatan  26066  log2cnv  26075  log2ublem3  26079  log2ub  26080  logfacbnd3  26352  bclbnd  26409  bpos1  26412  bposlem8  26420  lgsdilem  26453  lgsdir2lem1  26454  lgsdir2lem4  26457  lgsdir2lem5  26458  lgsdir2  26459  lgsdir  26461  2lgsoddprmlem3c  26541  dchrisum0flblem1  26637  rpvmasum2  26641  log2sumbnd  26673  ax5seglem7  27284  ex-fl  28790  ipasslem10  29180  hisubcomi  29445  normlem1  29451  normlem9  29459  norm-ii-i  29478  normsubi  29482  polid2i  29498  lnophmlem2  30358  lnfn0i  30383  nmopcoi  30436  unierri  30445  addltmulALT  30787  dpmul4  31167  sgnmul  32488  logdivsqrle  32609  hgt750lem  32610  hgt750lem2  32611  problem4  33605  quad3  33607  cnndvlem1  34696  sin2h  35746  poimirlem26  35782  cntotbnd  35933  60gcd6e6  39992  12lcm5e60  39996  60lcm7e420  39998  3lexlogpow5ineq1  40042  3lexlogpow5ineq5  40048  sqdeccom12  40297  ex-decpmul  40300  areaquad  41027  resqrtvalex  41206  imsqrtvalex  41207  coskpi2  43361  stoweidlem13  43508  wallispilem2  43561  wallispilem4  43563  wallispi2lem1  43566  dirkerper  43591  dirkertrigeqlem1  43593  dirkercncflem1  43598  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  257prm  44965  fmtnofac1  44974  fmtno4prmfac  44976  fmtno4nprmfac193  44978  fmtno5faclem1  44983  fmtno5faclem2  44984  139prmALT  45000  127prm  45003  11t31e341  45136  2exp340mod341  45137  nfermltl8rev  45146  tgoldbach  45221