Theorem mulid2i 10648

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  1c1 10540   · cmul 10544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  00id  10817  halfpm6th  11861  div4p1lem1div2  11895  3halfnz  12064  crreczi  13592  fac2  13642  hashxplem  13797  bpoly1  15407  bpoly2  15413  bpoly3  15414  bpoly4  15415  efival  15507  ef01bndlem  15539  3dvdsdec  15683  3dvds2dec  15684  odd2np1lem  15691  m1expo  15728  m1exp1  15729  nno  15735  divalglem5  15750  gcdaddmlem  15874  prmo2  16378  dec5nprm  16404  2exp8  16425  13prm  16451  23prm  16454  37prm  16456  43prm  16457  83prm  16458  139prm  16459  163prm  16460  317prm  16461  631prm  16462  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  cnmsgnsubg  20723  sin2pim  25073  cos2pim  25074  sincosq3sgn  25088  sincosq4sgn  25089  tangtx  25093  sincosq1eq  25100  sincos4thpi  25101  sincos6thpi  25103  pige3ALT  25107  abssinper  25108  ang180lem2  25390  ang180lem3  25391  1cubr  25422  asin1  25474  dvatan  25515  log2cnv  25524  log2ublem3  25528  log2ub  25529  logfacbnd3  25801  bclbnd  25858  bpos1  25861  bposlem8  25869  lgsdilem  25902  lgsdir2lem1  25903  lgsdir2lem4  25906  lgsdir2lem5  25907  lgsdir2  25908  lgsdir  25910  2lgsoddprmlem3c  25990  dchrisum0flblem1  26086  rpvmasum2  26090  log2sumbnd  26122  ax5seglem7  26723  ex-fl  28228  ipasslem10  28618  hisubcomi  28883  normlem1  28889  normlem9  28897  norm-ii-i  28916  normsubi  28920  polid2i  28936  lnophmlem2  29796  lnfn0i  29821  nmopcoi  29874  unierri  29883  addltmulALT  30225  dpmul4  30592  sgnmul  31802  logdivsqrle  31923  hgt750lem  31924  hgt750lem2  31925  problem4  32913  quad3  32915  cnndvlem1  33878  sin2h  34884  poimirlem26  34920  cntotbnd  35076  sqdeccom12  39182  ex-decpmul  39185  areaquad  39830  coskpi2  42154  stoweidlem13  42305  wallispilem2  42358  wallispilem4  42360  wallispi2lem1  42363  dirkerper  42388  dirkertrigeqlem1  42390  dirkercncflem1  42395  sqwvfoura  42520  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  257prm  43730  fmtnofac1  43739  fmtno4prmfac  43741  fmtno4nprmfac193  43743  fmtno5faclem1  43748  fmtno5faclem2  43749  139prmALT  43766  127prm  43770  11t31e341  43904  2exp340mod341  43905  nfermltl8rev  43914  tgoldbach  43989