Theorem mullidi 11186

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   · cmul 11080

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  00id  11356  div4p1lem1div2  12444  3halfnz  12620  crreczi  14200  fac2  14251  hashxplem  14405  bpoly1  16024  bpoly2  16030  bpoly3  16031  bpoly4  16032  efival  16127  ef01bndlem  16159  3dvdsdec  16309  3dvds2dec  16310  odd2np1lem  16317  m1expo  16352  m1exp1  16353  nno  16359  divalglem5  16374  gcdaddmlem  16501  prmo2  17018  dec5nprm  17044  2exp8  17066  13prm  17093  23prm  17096  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  cnmsgnsubg  21493  sin2pim  26401  cos2pim  26402  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sincosq1eq  26428  sincos4thpi  26429  sincos6thpi  26432  pige3ALT  26436  abssinper  26437  ang180lem2  26727  ang180lem3  26728  1cubr  26759  asin1  26811  dvatan  26852  log2cnv  26861  log2ublem3  26865  log2ub  26866  logfacbnd3  27141  bclbnd  27198  bpos1  27201  bposlem8  27209  lgsdilem  27242  lgsdir2lem1  27243  lgsdir2lem4  27246  lgsdir2lem5  27247  lgsdir2  27248  lgsdir  27250  2lgsoddprmlem3c  27330  dchrisum0flblem1  27426  rpvmasum2  27430  log2sumbnd  27462  ax5seglem7  28869  ex-fl  30383  ipasslem10  30775  hisubcomi  31040  normlem1  31046  normlem9  31054  norm-ii-i  31073  normsubi  31077  polid2i  31093  lnophmlem2  31953  lnfn0i  31978  nmopcoi  32031  unierri  32040  addltmulALT  32382  sgnmul  32767  dpmul4  32841  iconstr  33763  cos9thpiminplylem5  33783  logdivsqrle  34648  hgt750lem  34649  hgt750lem2  34650  problem4  35662  quad3  35664  cnndvlem1  36532  sin2h  37611  poimirlem26  37647  cntotbnd  37797  60gcd6e6  41999  12lcm5e60  42003  60lcm7e420  42005  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  sqdeccom12  42284  ex-decpmul  42301  1tiei  42312  sin2t3rdpi  42348  cos2t3rdpi  42349  areaquad  43212  resqrtvalex  43641  imsqrtvalex  43642  coskpi2  45871  stoweidlem13  46018  wallispilem2  46071  wallispilem4  46073  wallispi2lem1  46076  dirkerper  46101  dirkertrigeqlem1  46103  dirkercncflem1  46108  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  lamberte  46896  rehalfge1  47340  257prm  47566  fmtnofac1  47575  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno5faclem1  47584  fmtno5faclem2  47585  139prmALT  47601  127prm  47604  11t31e341  47737  2exp340mod341  47738  nfermltl8rev  47747  tgoldbach  47822