Theorem mullidi 11141

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  00id  11312  div4p1lem1div2  12423  3halfnz  12599  crreczi  14181  fac2  14232  hashxplem  14386  bpoly1  16007  bpoly2  16013  bpoly3  16014  bpoly4  16015  efival  16110  ef01bndlem  16142  3dvdsdec  16292  3dvds2dec  16293  odd2np1lem  16300  m1expo  16335  m1exp1  16336  nno  16342  divalglem5  16357  gcdaddmlem  16484  prmo2  17002  dec5nprm  17028  2exp8  17050  13prm  17077  23prm  17080  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  cnmsgnsubg  21567  sin2pim  26462  cos2pim  26463  sincosq3sgn  26477  sincosq4sgn  26478  tangtx  26482  sincosq1eq  26489  sincos4thpi  26490  sincos6thpi  26493  pige3ALT  26497  abssinper  26498  ang180lem2  26787  ang180lem3  26788  1cubr  26819  asin1  26871  dvatan  26912  log2cnv  26921  log2ublem3  26925  log2ub  26926  logfacbnd3  27200  bclbnd  27257  bpos1  27260  bposlem8  27268  lgsdilem  27301  lgsdir2lem1  27302  lgsdir2lem4  27305  lgsdir2lem5  27306  lgsdir2  27307  lgsdir  27309  2lgsoddprmlem3c  27389  dchrisum0flblem1  27485  rpvmasum2  27489  log2sumbnd  27521  ax5seglem7  29018  ex-fl  30532  ipasslem10  30925  hisubcomi  31190  normlem1  31196  normlem9  31204  norm-ii-i  31223  normsubi  31227  polid2i  31243  lnophmlem2  32103  lnfn0i  32128  nmopcoi  32181  unierri  32190  addltmulALT  32532  sgnmul  32923  dpmul4  32988  iconstr  33926  cos9thpiminplylem5  33946  logdivsqrle  34810  hgt750lem  34811  hgt750lem2  34812  problem4  35866  quad3  35868  cnndvlem1  36813  sin2h  37945  poimirlem26  37981  cntotbnd  38131  60gcd6e6  42457  12lcm5e60  42461  60lcm7e420  42463  3lexlogpow5ineq1  42507  3lexlogpow5ineq5  42513  sqdeccom12  42735  ex-decpmul  42752  1tiei  42763  sin2t3rdpi  42799  cos2t3rdpi  42800  areaquad  43662  resqrtvalex  44090  imsqrtvalex  44091  coskpi2  46312  stoweidlem13  46459  wallispilem2  46512  wallispilem4  46514  wallispi2lem1  46517  dirkerper  46542  dirkertrigeqlem1  46544  dirkercncflem1  46549  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  lamberte  47348  rehalfge1  47799  257prm  48036  fmtnofac1  48045  fmtno4prmfac  48047  fmtno4nprmfac193  48049  fmtno5faclem1  48054  fmtno5faclem2  48055  139prmALT  48071  127prm  48074  11t31e341  48220  2exp340mod341  48221  nfermltl8rev  48230  tgoldbach  48305