Theorem mulid2i 10363

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

Syntax hints:   = wceq 1658   ∈ wcel 2166  (class class class)co 6906  ℂcc 10251  1c1 10254   · cmul 10258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-mulcl 10315  ax-mulcom 10317  ax-mulass 10319  ax-distr 10320  ax-1rid 10323  ax-cnre 10326

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-ov 6909

This theorem is referenced by:  00id  10531  halfpm6th  11580  div4p1lem1div2  11614  3halfnz  11785  crreczi  13284  fac2  13360  hashxplem  13510  bpoly1  15155  bpoly2  15161  bpoly3  15162  bpoly4  15163  efival  15255  ef01bndlem  15287  3dvdsdec  15431  3dvds2dec  15432  odd2np1lem  15439  m1expo  15467  m1exp1  15468  nno  15473  divalglem5  15495  gcdaddmlem  15619  prmo2  16116  dec5nprm  16142  2exp8  16163  13prm  16189  23prm  16192  37prm  16194  43prm  16195  83prm  16196  139prm  16197  163prm  16198  317prm  16199  631prm  16200  1259lem2  16205  1259lem3  16206  1259lem4  16207  1259lem5  16208  2503lem1  16210  2503lem2  16211  2503lem3  16212  2503prm  16213  4001lem1  16214  4001lem2  16215  4001lem3  16216  4001lem4  16217  cnmsgnsubg  20283  sin2pim  24638  cos2pim  24639  sincosq3sgn  24653  sincosq4sgn  24654  tangtx  24658  sincosq1eq  24665  sincos4thpi  24666  sincos6thpi  24668  pige3  24670  abssinper  24671  ang180lem2  24951  ang180lem3  24952  1cubr  24983  asin1  25035  dvatan  25076  log2cnv  25085  log2ublem3  25089  log2ub  25090  logfacbnd3  25362  bclbnd  25419  bpos1  25422  bposlem8  25430  lgsdilem  25463  lgsdir2lem1  25464  lgsdir2lem4  25467  lgsdir2lem5  25468  lgsdir2  25469  lgsdir  25471  2lgsoddprmlem3c  25551  dchrisum0flblem1  25611  rpvmasum2  25615  log2sumbnd  25647  ax5seglem7  26235  ex-fl  27863  ipasslem10  28250  hisubcomi  28517  normlem1  28523  normlem9  28531  norm-ii-i  28550  normsubi  28554  polid2i  28570  lnophmlem2  29432  lnfn0i  29457  nmopcoi  29510  unierri  29519  addltmulALT  29861  dpmul4  30168  sgnmul  31151  logdivsqrle  31278  hgt750lem  31279  hgt750lem2  31280  problem4  32107  quad3  32109  cnndvlem1  33061  sin2h  33943  poimirlem26  33980  cntotbnd  34138  sqdeccom12  38065  ex-decpmul  38068  areaquad  38645  coskpi2  40873  stoweidlem13  41025  wallispilem2  41078  wallispilem4  41080  wallispi2lem1  41083  dirkerper  41108  dirkertrigeqlem1  41110  dirkercncflem1  41115  sqwvfoura  41240  sqwvfourb  41241  fourierswlem  41242  fouriersw  41243  257prm  42304  fmtnofac1  42313  fmtno4prmfac  42315  fmtno4nprmfac193  42317  fmtno5faclem1  42322  fmtno5faclem2  42323  139prmALT  42342  127prm  42346  tgoldbach  42536