Theorem mulid2i 10081

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

Syntax hints:   = wceq 1523   ∈ wcel 2030  (class class class)co 6690  ℂcc 9972  1c1 9975   · cmul 9979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-mulcom 10038  ax-mulass 10040  ax-distr 10041  ax-1rid 10044  ax-cnre 10047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693

This theorem is referenced by:  00id  10249  halfpm6th  11291  div4p1lem1div2  11325  3halfnz  11494  crreczi  13029  sq10  13088  fac2  13106  hashxplem  13258  bpoly1  14826  bpoly2  14832  bpoly3  14833  bpoly4  14834  efival  14926  ef01bndlem  14958  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  odd2np1lem  15111  m1expo  15139  m1exp1  15140  nno  15145  divalglem5  15167  gcdaddmlem  15292  prmo2  15791  dec5nprm  15817  2exp8  15843  13prm  15870  23prm  15873  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  cnmsgnsubg  19971  sin2pim  24282  cos2pim  24283  sincosq3sgn  24297  sincosq4sgn  24298  tangtx  24302  sincosq1eq  24309  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  abssinper  24315  ang180lem2  24585  ang180lem3  24586  1cubr  24614  asin1  24666  dvatan  24707  log2cnv  24716  log2ublem3  24720  log2ub  24721  logfacbnd3  24993  bclbnd  25050  bpos1  25053  bposlem8  25061  lgsdilem  25094  lgsdir2lem1  25095  lgsdir2lem4  25098  lgsdir2lem5  25099  lgsdir2  25100  lgsdir  25102  2lgsoddprmlem3c  25182  dchrisum0flblem1  25242  rpvmasum2  25246  log2sumbnd  25278  ax5seglem7  25860  ex-fl  27434  ipasslem10  27822  hisubcomi  28089  normlem1  28095  normlem9  28103  norm-ii-i  28122  normsubi  28126  polid2i  28142  lnophmlem2  29004  lnfn0i  29029  nmopcoi  29082  unierri  29091  addltmulALT  29433  dpmul4  29750  sgnmul  30732  logdivsqrle  30856  hgt750lem  30857  hgt750lem2  30858  problem4  31688  quad3  31690  cnndvlem1  32653  sin2h  33529  poimirlem26  33565  cntotbnd  33725  areaquad  38119  coskpi2  40395  stoweidlem13  40548  wallispilem2  40601  wallispilem4  40603  wallispi2lem1  40606  dirkerper  40631  dirkertrigeqlem1  40633  dirkercncflem1  40638  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  257prm  41798  fmtnofac1  41807  fmtno4prmfac  41809  fmtno4nprmfac193  41811  fmtno5faclem1  41816  fmtno5faclem2  41817  139prmALT  41836  127prm  41840  tgoldbach  42030  tgoldbachOLD  42037