Theorem mulid2i 10886

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

Syntax hints:   = wceq 1543   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775  1c1 10778   · cmul 10782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-mulcl 10839  ax-mulcom 10841  ax-mulass 10843  ax-distr 10844  ax-1rid 10847  ax-cnre 10850

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6373  df-fv 6423  df-ov 7255

This theorem is referenced by:  00id  11055  halfpm6th  12099  div4p1lem1div2  12133  3halfnz  12304  crreczi  13846  fac2  13896  hashxplem  14051  bpoly1  15664  bpoly2  15670  bpoly3  15671  bpoly4  15672  efival  15764  ef01bndlem  15796  3dvdsdec  15944  3dvds2dec  15945  odd2np1lem  15952  m1expo  15987  m1exp1  15988  nno  15994  divalglem5  16009  gcdaddmlem  16134  prmo2  16644  dec5nprm  16670  2exp8  16693  13prm  16720  23prm  16723  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  cnmsgnsubg  20669  sin2pim  25522  cos2pim  25523  sincosq3sgn  25537  sincosq4sgn  25538  tangtx  25542  sincosq1eq  25549  sincos4thpi  25550  sincos6thpi  25552  pige3ALT  25556  abssinper  25557  ang180lem2  25840  ang180lem3  25841  1cubr  25872  asin1  25924  dvatan  25965  log2cnv  25974  log2ublem3  25978  log2ub  25979  logfacbnd3  26251  bclbnd  26308  bpos1  26311  bposlem8  26319  lgsdilem  26352  lgsdir2lem1  26353  lgsdir2lem4  26356  lgsdir2lem5  26357  lgsdir2  26358  lgsdir  26360  2lgsoddprmlem3c  26440  dchrisum0flblem1  26536  rpvmasum2  26540  log2sumbnd  26572  ax5seglem7  27181  ex-fl  28687  ipasslem10  29077  hisubcomi  29342  normlem1  29348  normlem9  29356  norm-ii-i  29375  normsubi  29379  polid2i  29395  lnophmlem2  30255  lnfn0i  30280  nmopcoi  30333  unierri  30342  addltmulALT  30684  dpmul4  31065  sgnmul  32384  logdivsqrle  32505  hgt750lem  32506  hgt750lem2  32507  problem4  33501  quad3  33503  cnndvlem1  34619  sin2h  35673  poimirlem26  35709  cntotbnd  35860  60gcd6e6  39919  12lcm5e60  39923  60lcm7e420  39925  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  sqdeccom12  40210  ex-decpmul  40213  areaquad  40935  resqrtvalex  41114  imsqrtvalex  41115  coskpi2  43270  stoweidlem13  43417  wallispilem2  43470  wallispilem4  43472  wallispi2lem1  43475  dirkerper  43500  dirkertrigeqlem1  43502  dirkercncflem1  43507  sqwvfoura  43632  sqwvfourb  43633  fourierswlem  43634  fouriersw  43635  257prm  44874  fmtnofac1  44883  fmtno4prmfac  44885  fmtno4nprmfac193  44887  fmtno5faclem1  44892  fmtno5faclem2  44893  139prmALT  44909  127prm  44912  11t31e341  45045  2exp340mod341  45046  nfermltl8rev  45055  tgoldbach  45130