Theorem mullidi 11226

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11114  1c1 11117   · cmul 11121

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-mulcl 11178  ax-mulcom 11180  ax-mulass 11182  ax-distr 11183  ax-1rid 11186  ax-cnre 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415

This theorem is referenced by:  00id  11396  halfpm6th  12440  div4p1lem1div2  12474  3halfnz  12648  crreczi  14198  fac2  14246  hashxplem  14400  bpoly1  16002  bpoly2  16008  bpoly3  16009  bpoly4  16010  efival  16102  ef01bndlem  16134  3dvdsdec  16282  3dvds2dec  16283  odd2np1lem  16290  m1expo  16325  m1exp1  16326  nno  16332  divalglem5  16347  gcdaddmlem  16472  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  21441  sin2pim  26336  cos2pim  26337  sincosq3sgn  26351  sincosq4sgn  26352  tangtx  26356  sincosq1eq  26363  sincos4thpi  26364  sincos6thpi  26366  pige3ALT  26370  abssinper  26371  ang180lem2  26657  ang180lem3  26658  1cubr  26689  asin1  26741  dvatan  26782  log2cnv  26791  log2ublem3  26795  log2ub  26796  logfacbnd3  27071  bclbnd  27128  bpos1  27131  bposlem8  27139  lgsdilem  27172  lgsdir2lem1  27173  lgsdir2lem4  27176  lgsdir2lem5  27177  lgsdir2  27178  lgsdir  27180  2lgsoddprmlem3c  27260  dchrisum0flblem1  27356  rpvmasum2  27360  log2sumbnd  27392  ax5seglem7  28628  ex-fl  30135  ipasslem10  30527  hisubcomi  30792  normlem1  30798  normlem9  30806  norm-ii-i  30825  normsubi  30829  polid2i  30845  lnophmlem2  31705  lnfn0i  31730  nmopcoi  31783  unierri  31792  addltmulALT  32134  dpmul4  32515  sgnmul  34007  logdivsqrle  34128  hgt750lem  34129  hgt750lem2  34130  problem4  35119  quad3  35121  cnndvlem1  35880  sin2h  36945  poimirlem26  36981  cntotbnd  37131  60gcd6e6  41339  12lcm5e60  41343  60lcm7e420  41345  3lexlogpow5ineq1  41389  3lexlogpow5ineq5  41395  sqdeccom12  41667  ex-decpmul  41672  areaquad  42431  resqrtvalex  42862  imsqrtvalex  42863  coskpi2  45044  stoweidlem13  45191  wallispilem2  45244  wallispilem4  45246  wallispi2lem1  45249  dirkerper  45274  dirkertrigeqlem1  45276  dirkercncflem1  45281  sqwvfoura  45406  sqwvfourb  45407  fourierswlem  45408  fouriersw  45409  257prm  46691  fmtnofac1  46700  fmtno4prmfac  46702  fmtno4nprmfac193  46704  fmtno5faclem1  46709  fmtno5faclem2  46710  139prmALT  46726  127prm  46729  11t31e341  46862  2exp340mod341  46863  nfermltl8rev  46872  tgoldbach  46947