Theorem mullidi 11117

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   · cmul 11011

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  00id  11288  div4p1lem1div2  12376  3halfnz  12552  crreczi  14135  fac2  14186  hashxplem  14340  bpoly1  15958  bpoly2  15964  bpoly3  15965  bpoly4  15966  efival  16061  ef01bndlem  16093  3dvdsdec  16243  3dvds2dec  16244  odd2np1lem  16251  m1expo  16286  m1exp1  16287  nno  16293  divalglem5  16308  gcdaddmlem  16435  prmo2  16952  dec5nprm  16978  2exp8  17000  13prm  17027  23prm  17030  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  cnmsgnsubg  21515  sin2pim  26422  cos2pim  26423  sincosq3sgn  26437  sincosq4sgn  26438  tangtx  26442  sincosq1eq  26449  sincos4thpi  26450  sincos6thpi  26453  pige3ALT  26457  abssinper  26458  ang180lem2  26748  ang180lem3  26749  1cubr  26780  asin1  26832  dvatan  26873  log2cnv  26882  log2ublem3  26886  log2ub  26887  logfacbnd3  27162  bclbnd  27219  bpos1  27222  bposlem8  27230  lgsdilem  27263  lgsdir2lem1  27264  lgsdir2lem4  27267  lgsdir2lem5  27268  lgsdir2  27269  lgsdir  27271  2lgsoddprmlem3c  27351  dchrisum0flblem1  27447  rpvmasum2  27451  log2sumbnd  27483  ax5seglem7  28914  ex-fl  30425  ipasslem10  30817  hisubcomi  31082  normlem1  31088  normlem9  31096  norm-ii-i  31115  normsubi  31119  polid2i  31135  lnophmlem2  31995  lnfn0i  32020  nmopcoi  32073  unierri  32082  addltmulALT  32424  sgnmul  32816  dpmul4  32892  iconstr  33777  cos9thpiminplylem5  33797  logdivsqrle  34661  hgt750lem  34662  hgt750lem2  34663  problem4  35710  quad3  35712  cnndvlem1  36577  sin2h  37656  poimirlem26  37692  cntotbnd  37842  60gcd6e6  42043  12lcm5e60  42047  60lcm7e420  42049  3lexlogpow5ineq1  42093  3lexlogpow5ineq5  42099  sqdeccom12  42328  ex-decpmul  42345  1tiei  42356  sin2t3rdpi  42392  cos2t3rdpi  42393  areaquad  43255  resqrtvalex  43684  imsqrtvalex  43685  coskpi2  45910  stoweidlem13  46057  wallispilem2  46110  wallispilem4  46112  wallispi2lem1  46115  dirkerper  46140  dirkertrigeqlem1  46142  dirkercncflem1  46147  sqwvfoura  46272  sqwvfourb  46273  fourierswlem  46274  fouriersw  46275  lamberte  46925  rehalfge1  47372  257prm  47598  fmtnofac1  47607  fmtno4prmfac  47609  fmtno4nprmfac193  47611  fmtno5faclem1  47616  fmtno5faclem2  47617  139prmALT  47633  127prm  47636  11t31e341  47769  2exp340mod341  47770  nfermltl8rev  47779  tgoldbach  47854