Theorem mullidi 11232

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  (class class class)co 7399  ℂcc 11119  1c1 11122   · cmul 11126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-mulcl 11183  ax-mulcom 11185  ax-mulass 11187  ax-distr 11188  ax-1rid 11191  ax-cnre 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402

This theorem is referenced by:  00id  11402  div4p1lem1div2  12488  3halfnz  12664  crreczi  14234  fac2  14285  hashxplem  14439  bpoly1  16054  bpoly2  16060  bpoly3  16061  bpoly4  16062  efival  16155  ef01bndlem  16187  3dvdsdec  16336  3dvds2dec  16337  odd2np1lem  16344  m1expo  16379  m1exp1  16380  nno  16386  divalglem5  16401  gcdaddmlem  16528  prmo2  17045  dec5nprm  17071  2exp8  17093  13prm  17120  23prm  17123  37prm  17125  43prm  17126  83prm  17127  139prm  17128  163prm  17129  317prm  17130  631prm  17131  1259lem2  17136  1259lem3  17137  1259lem4  17138  1259lem5  17139  2503lem1  17141  2503lem2  17142  2503lem3  17143  2503prm  17144  4001lem1  17145  4001lem2  17146  4001lem3  17147  4001lem4  17148  cnmsgnsubg  21522  sin2pim  26430  cos2pim  26431  sincosq3sgn  26445  sincosq4sgn  26446  tangtx  26450  sincosq1eq  26457  sincos4thpi  26458  sincos6thpi  26461  pige3ALT  26465  abssinper  26466  ang180lem2  26756  ang180lem3  26757  1cubr  26788  asin1  26840  dvatan  26881  log2cnv  26890  log2ublem3  26894  log2ub  26895  logfacbnd3  27170  bclbnd  27227  bpos1  27230  bposlem8  27238  lgsdilem  27271  lgsdir2lem1  27272  lgsdir2lem4  27275  lgsdir2lem5  27276  lgsdir2  27277  lgsdir  27279  2lgsoddprmlem3c  27359  dchrisum0flblem1  27455  rpvmasum2  27459  log2sumbnd  27491  ax5seglem7  28846  ex-fl  30360  ipasslem10  30752  hisubcomi  31017  normlem1  31023  normlem9  31031  norm-ii-i  31050  normsubi  31054  polid2i  31070  lnophmlem2  31930  lnfn0i  31955  nmopcoi  32008  unierri  32017  addltmulALT  32359  dpmul4  32806  iconstr  33716  sgnmul  34483  logdivsqrle  34603  hgt750lem  34604  hgt750lem2  34605  problem4  35611  quad3  35613  cnndvlem1  36476  sin2h  37555  poimirlem26  37591  cntotbnd  37741  60gcd6e6  41939  12lcm5e60  41943  60lcm7e420  41945  3lexlogpow5ineq1  41989  3lexlogpow5ineq5  41995  sqdeccom12  42262  ex-decpmul  42278  1tiei  42290  areaquad  43165  resqrtvalex  43594  imsqrtvalex  43595  coskpi2  45825  stoweidlem13  45972  wallispilem2  46025  wallispilem4  46027  wallispi2lem1  46030  dirkerper  46055  dirkertrigeqlem1  46057  dirkercncflem1  46062  sqwvfoura  46187  sqwvfourb  46188  fourierswlem  46189  fouriersw  46190  257prm  47493  fmtnofac1  47502  fmtno4prmfac  47504  fmtno4nprmfac193  47506  fmtno5faclem1  47511  fmtno5faclem2  47512  139prmALT  47528  127prm  47531  11t31e341  47664  2exp340mod341  47665  nfermltl8rev  47674  tgoldbach  47749