Theorem mullidi 11220

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mullidi	⊢ (1 · 𝐴) = 𝐴

Proof of Theorem mullidi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mullid 11214	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7404  ℂcc 11107  1c1 11110   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407

This theorem is referenced by:  00id  11390  halfpm6th  12434  div4p1lem1div2  12468  3halfnz  12642  crreczi  14194  fac2  14242  hashxplem  14396  bpoly1  15999  bpoly2  16005  bpoly3  16006  bpoly4  16007  efival  16100  ef01bndlem  16132  3dvdsdec  16280  3dvds2dec  16281  odd2np1lem  16288  m1expo  16323  m1exp1  16324  nno  16330  divalglem5  16345  gcdaddmlem  16470  prmo2  16980  dec5nprm  17006  2exp8  17029  13prm  17056  23prm  17059  37prm  17061  43prm  17062  83prm  17063  139prm  17064  163prm  17065  317prm  17066  631prm  17067  1259lem2  17072  1259lem3  17073  1259lem4  17074  1259lem5  17075  2503lem1  17077  2503lem2  17078  2503lem3  17079  2503prm  17080  4001lem1  17081  4001lem2  17082  4001lem3  17083  4001lem4  17084  cnmsgnsubg  21466  sin2pim  26371  cos2pim  26372  sincosq3sgn  26386  sincosq4sgn  26387  tangtx  26391  sincosq1eq  26398  sincos4thpi  26399  sincos6thpi  26401  pige3ALT  26405  abssinper  26406  ang180lem2  26693  ang180lem3  26694  1cubr  26725  asin1  26777  dvatan  26818  log2cnv  26827  log2ublem3  26831  log2ub  26832  logfacbnd3  27107  bclbnd  27164  bpos1  27167  bposlem8  27175  lgsdilem  27208  lgsdir2lem1  27209  lgsdir2lem4  27212  lgsdir2lem5  27213  lgsdir2  27214  lgsdir  27216  2lgsoddprmlem3c  27296  dchrisum0flblem1  27392  rpvmasum2  27396  log2sumbnd  27428  ax5seglem7  28697  ex-fl  30205  ipasslem10  30597  hisubcomi  30862  normlem1  30868  normlem9  30876  norm-ii-i  30895  normsubi  30899  polid2i  30915  lnophmlem2  31775  lnfn0i  31800  nmopcoi  31853  unierri  31862  addltmulALT  32204  dpmul4  32583  sgnmul  34071  logdivsqrle  34191  hgt750lem  34192  hgt750lem2  34193  problem4  35181  quad3  35183  cnndvlem1  35921  sin2h  36989  poimirlem26  37025  cntotbnd  37175  60gcd6e6  41383  12lcm5e60  41387  60lcm7e420  41389  3lexlogpow5ineq1  41433  3lexlogpow5ineq5  41439  sqdeccom12  41740  ex-decpmul  41745  1tiei  41755  areaquad  42522  resqrtvalex  42953  imsqrtvalex  42954  coskpi2  45135  stoweidlem13  45282  wallispilem2  45335  wallispilem4  45337  wallispi2lem1  45340  dirkerper  45365  dirkertrigeqlem1  45367  dirkercncflem1  45372  sqwvfoura  45497  sqwvfourb  45498  fourierswlem  45499  fouriersw  45500  257prm  46782  fmtnofac1  46791  fmtno4prmfac  46793  fmtno4nprmfac193  46795  fmtno5faclem1  46800  fmtno5faclem2  46801  139prmALT  46817  127prm  46820  11t31e341  46953  2exp340mod341  46954  nfermltl8rev  46963  tgoldbach  47038