Theorem mullidi 11139

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  00id  11309  div4p1lem1div2  12397  3halfnz  12573  crreczi  14153  fac2  14204  hashxplem  14358  bpoly1  15976  bpoly2  15982  bpoly3  15983  bpoly4  15984  efival  16079  ef01bndlem  16111  3dvdsdec  16261  3dvds2dec  16262  odd2np1lem  16269  m1expo  16304  m1exp1  16305  nno  16311  divalglem5  16326  gcdaddmlem  16453  prmo2  16970  dec5nprm  16996  2exp8  17018  13prm  17045  23prm  17048  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  cnmsgnsubg  21502  sin2pim  26410  cos2pim  26411  sincosq3sgn  26425  sincosq4sgn  26426  tangtx  26430  sincosq1eq  26437  sincos4thpi  26438  sincos6thpi  26441  pige3ALT  26445  abssinper  26446  ang180lem2  26736  ang180lem3  26737  1cubr  26768  asin1  26820  dvatan  26861  log2cnv  26870  log2ublem3  26874  log2ub  26875  logfacbnd3  27150  bclbnd  27207  bpos1  27210  bposlem8  27218  lgsdilem  27251  lgsdir2lem1  27252  lgsdir2lem4  27255  lgsdir2lem5  27256  lgsdir2  27257  lgsdir  27259  2lgsoddprmlem3c  27339  dchrisum0flblem1  27435  rpvmasum2  27439  log2sumbnd  27471  ax5seglem7  28898  ex-fl  30409  ipasslem10  30801  hisubcomi  31066  normlem1  31072  normlem9  31080  norm-ii-i  31099  normsubi  31103  polid2i  31119  lnophmlem2  31979  lnfn0i  32004  nmopcoi  32057  unierri  32066  addltmulALT  32408  sgnmul  32793  dpmul4  32867  iconstr  33732  cos9thpiminplylem5  33752  logdivsqrle  34617  hgt750lem  34618  hgt750lem2  34619  problem4  35640  quad3  35642  cnndvlem1  36510  sin2h  37589  poimirlem26  37625  cntotbnd  37775  60gcd6e6  41977  12lcm5e60  41981  60lcm7e420  41983  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  sqdeccom12  42262  ex-decpmul  42279  1tiei  42290  sin2t3rdpi  42326  cos2t3rdpi  42327  areaquad  43189  resqrtvalex  43618  imsqrtvalex  43619  coskpi2  45848  stoweidlem13  45995  wallispilem2  46048  wallispilem4  46050  wallispi2lem1  46053  dirkerper  46078  dirkertrigeqlem1  46080  dirkercncflem1  46085  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  lamberte  46873  rehalfge1  47320  257prm  47546  fmtnofac1  47555  fmtno4prmfac  47557  fmtno4nprmfac193  47559  fmtno5faclem1  47564  fmtno5faclem2  47565  139prmALT  47581  127prm  47584  11t31e341  47717  2exp340mod341  47718  nfermltl8rev  47727  tgoldbach  47802