Theorem mullidi 11257

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144  1c1 11147   · cmul 11151

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 2699  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-mulcl 11208  ax-mulcom 11210  ax-mulass 11212  ax-distr 11213  ax-1rid 11216  ax-cnre 11219

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429

This theorem is referenced by:  00id  11427  halfpm6th  12471  div4p1lem1div2  12505  3halfnz  12679  crreczi  14230  fac2  14278  hashxplem  14432  bpoly1  16035  bpoly2  16041  bpoly3  16042  bpoly4  16043  efival  16136  ef01bndlem  16168  3dvdsdec  16316  3dvds2dec  16317  odd2np1lem  16324  m1expo  16359  m1exp1  16360  nno  16366  divalglem5  16381  gcdaddmlem  16506  prmo2  17016  dec5nprm  17042  2exp8  17065  13prm  17092  23prm  17095  37prm  17097  43prm  17098  83prm  17099  139prm  17100  163prm  17101  317prm  17102  631prm  17103  1259lem2  17108  1259lem3  17109  1259lem4  17110  1259lem5  17111  2503lem1  17113  2503lem2  17114  2503lem3  17115  2503prm  17116  4001lem1  17117  4001lem2  17118  4001lem3  17119  4001lem4  17120  cnmsgnsubg  21516  sin2pim  26440  cos2pim  26441  sincosq3sgn  26455  sincosq4sgn  26456  tangtx  26460  sincosq1eq  26467  sincos4thpi  26468  sincos6thpi  26470  pige3ALT  26474  abssinper  26475  ang180lem2  26762  ang180lem3  26763  1cubr  26794  asin1  26846  dvatan  26887  log2cnv  26896  log2ublem3  26900  log2ub  26901  logfacbnd3  27176  bclbnd  27233  bpos1  27236  bposlem8  27244  lgsdilem  27277  lgsdir2lem1  27278  lgsdir2lem4  27281  lgsdir2lem5  27282  lgsdir2  27283  lgsdir  27285  2lgsoddprmlem3c  27365  dchrisum0flblem1  27461  rpvmasum2  27465  log2sumbnd  27497  ax5seglem7  28766  ex-fl  30277  ipasslem10  30669  hisubcomi  30934  normlem1  30940  normlem9  30948  norm-ii-i  30967  normsubi  30971  polid2i  30987  lnophmlem2  31847  lnfn0i  31872  nmopcoi  31925  unierri  31934  addltmulALT  32276  dpmul4  32658  sgnmul  34195  logdivsqrle  34315  hgt750lem  34316  hgt750lem2  34317  problem4  35305  quad3  35307  cnndvlem1  36045  sin2h  37116  poimirlem26  37152  cntotbnd  37302  60gcd6e6  41507  12lcm5e60  41511  60lcm7e420  41513  3lexlogpow5ineq1  41557  3lexlogpow5ineq5  41563  sqdeccom12  41894  ex-decpmul  41899  1tiei  41909  areaquad  42675  resqrtvalex  43106  imsqrtvalex  43107  coskpi2  45283  stoweidlem13  45430  wallispilem2  45483  wallispilem4  45485  wallispi2lem1  45488  dirkerper  45513  dirkertrigeqlem1  45515  dirkercncflem1  45520  sqwvfoura  45645  sqwvfourb  45646  fourierswlem  45647  fouriersw  45648  257prm  46930  fmtnofac1  46939  fmtno4prmfac  46941  fmtno4nprmfac193  46943  fmtno5faclem1  46948  fmtno5faclem2  46949  139prmALT  46965  127prm  46968  11t31e341  47101  2exp340mod341  47102  nfermltl8rev  47111  tgoldbach  47186