Theorem mullidi 11184

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulcom 11134  ax-mulass 11136  ax-distr 11137  ax-1rid 11140  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  00id  11355  div4p1lem1div2  12473  3halfnz  12649  crreczi  14238  fac2  14289  hashxplem  14443  bpoly1  16064  bpoly2  16070  bpoly3  16071  bpoly4  16072  efival  16167  ef01bndlem  16199  3dvdsdec  16349  3dvds2dec  16350  odd2np1lem  16357  m1expo  16392  m1exp1  16393  nno  16399  divalglem5  16414  gcdaddmlem  16541  prmo2  17059  dec5nprm  17085  2exp8  17107  13prm  17135  23prm  17138  37prm  17140  43prm  17141  83prm  17142  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  2503lem1  17156  2503lem2  17157  2503lem3  17158  2503prm  17159  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  cnmsgnsubg  21609  sin2pim  26527  cos2pim  26528  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sincosq1eq  26554  sincos4thpi  26555  sincos6thpi  26558  pige3ALT  26562  abssinper  26563  ang180lem2  26852  ang180lem3  26853  1cubr  26884  asin1  26936  dvatan  26977  log2cnv  26986  log2ublem3  26990  log2ub  26991  logfacbnd3  27264  bclbnd  27321  bpos1  27324  bposlem8  27332  lgsdilem  27365  lgsdir2lem1  27366  lgsdir2lem4  27369  lgsdir2lem5  27370  lgsdir2  27371  lgsdir  27373  2lgsoddprmlem3c  27453  dchrisum0flblem1  27549  rpvmasum2  27553  log2sumbnd  27585  ax5seglem7  29082  ex-fl  30595  ipasslem10  30988  hisubcomi  31253  normlem1  31259  normlem9  31267  norm-ii-i  31286  normsubi  31290  polid2i  31306  lnophmlem2  32166  lnfn0i  32191  nmopcoi  32244  unierri  32253  addltmulALT  32595  sgnmul  32987  dpmul4  33052  iconstr  34024  cos9thpiminplylem5  34044  logdivsqrle  34908  hgt750lem  34909  hgt750lem2  34910  problem4  35982  quad3  35984  cnndvlem1  36939  sin2h  38073  poimirlem26  38109  cntotbnd  38259  60gcd6e6  42585  12lcm5e60  42589  60lcm7e420  42591  3lexlogpow5ineq1  42635  3lexlogpow5ineq5  42641  sqdeccom12  42862  ex-decpmul  42879  1tiei  42890  sin2t3rdpi  42926  cos2t3rdpi  42927  areaquad  43757  resqrtvalex  44185  imsqrtvalex  44186  coskpi2  46404  stoweidlem13  46551  wallispilem2  46604  wallispilem4  46606  wallispi2lem1  46609  dirkerper  46634  dirkertrigeqlem1  46636  dirkercncflem1  46641  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  cos5t  47437  lamberte  47446  rehalfge1  47897  257prm  48134  fmtnofac1  48143  fmtno4prmfac  48145  fmtno4nprmfac193  48147  fmtno5faclem1  48152  fmtno5faclem2  48153  139prmALT  48169  127prm  48172  11t31e341  48318  2exp340mod341  48319  nfermltl8rev  48328  tgoldbach  48403