Theorem mullidi 11148

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulcom 11100  ax-mulass 11102  ax-distr 11103  ax-1rid 11106  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  00id  11319  div4p1lem1div2  12430  3halfnz  12606  crreczi  14188  fac2  14239  hashxplem  14393  bpoly1  16014  bpoly2  16020  bpoly3  16021  bpoly4  16022  efival  16117  ef01bndlem  16149  3dvdsdec  16299  3dvds2dec  16300  odd2np1lem  16307  m1expo  16342  m1exp1  16343  nno  16349  divalglem5  16364  gcdaddmlem  16491  prmo2  17009  dec5nprm  17035  2exp8  17057  13prm  17084  23prm  17087  37prm  17089  43prm  17090  83prm  17091  139prm  17092  163prm  17093  317prm  17094  631prm  17095  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  2503lem1  17105  2503lem2  17106  2503lem3  17107  2503prm  17108  4001lem1  17109  4001lem2  17110  4001lem3  17111  4001lem4  17112  cnmsgnsubg  21559  sin2pim  26474  cos2pim  26475  sincosq3sgn  26489  sincosq4sgn  26490  tangtx  26494  sincosq1eq  26501  sincos4thpi  26502  sincos6thpi  26505  pige3ALT  26509  abssinper  26510  ang180lem2  26799  ang180lem3  26800  1cubr  26831  asin1  26883  dvatan  26924  log2cnv  26933  log2ublem3  26937  log2ub  26938  logfacbnd3  27211  bclbnd  27268  bpos1  27271  bposlem8  27279  lgsdilem  27312  lgsdir2lem1  27313  lgsdir2lem4  27316  lgsdir2lem5  27317  lgsdir2  27318  lgsdir  27320  2lgsoddprmlem3c  27400  dchrisum0flblem1  27496  rpvmasum2  27500  log2sumbnd  27532  ax5seglem7  29029  ex-fl  30542  ipasslem10  30935  hisubcomi  31200  normlem1  31206  normlem9  31214  norm-ii-i  31233  normsubi  31237  polid2i  31253  lnophmlem2  32113  lnfn0i  32138  nmopcoi  32191  unierri  32200  addltmulALT  32542  sgnmul  32934  dpmul4  32999  iconstr  33957  cos9thpiminplylem5  33977  logdivsqrle  34841  hgt750lem  34842  hgt750lem2  34843  problem4  35903  quad3  35905  cnndvlem1  36850  sin2h  37984  poimirlem26  38020  cntotbnd  38170  60gcd6e6  42496  12lcm5e60  42500  60lcm7e420  42502  3lexlogpow5ineq1  42546  3lexlogpow5ineq5  42552  sqdeccom12  42773  ex-decpmul  42790  1tiei  42801  sin2t3rdpi  42837  cos2t3rdpi  42838  areaquad  43668  resqrtvalex  44096  imsqrtvalex  44097  coskpi2  46316  stoweidlem13  46463  wallispilem2  46516  wallispilem4  46518  wallispi2lem1  46521  dirkerper  46546  dirkertrigeqlem1  46548  dirkercncflem1  46553  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  cos5t  47349  lamberte  47358  rehalfge1  47809  257prm  48046  fmtnofac1  48055  fmtno4prmfac  48057  fmtno4nprmfac193  48059  fmtno5faclem1  48064  fmtno5faclem2  48065  139prmALT  48081  127prm  48084  11t31e341  48230  2exp340mod341  48231  nfermltl8rev  48240  tgoldbach  48315