Theorem mullidi 11266

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  00id  11436  halfpm6th  12487  div4p1lem1div2  12521  3halfnz  12697  crreczi  14267  fac2  14318  hashxplem  14472  bpoly1  16087  bpoly2  16093  bpoly3  16094  bpoly4  16095  efival  16188  ef01bndlem  16220  3dvdsdec  16369  3dvds2dec  16370  odd2np1lem  16377  m1expo  16412  m1exp1  16413  nno  16419  divalglem5  16434  gcdaddmlem  16561  prmo2  17078  dec5nprm  17104  2exp8  17126  13prm  17153  23prm  17156  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  cnmsgnsubg  21595  sin2pim  26527  cos2pim  26528  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sincosq1eq  26554  sincos4thpi  26555  sincos6thpi  26558  pige3ALT  26562  abssinper  26563  ang180lem2  26853  ang180lem3  26854  1cubr  26885  asin1  26937  dvatan  26978  log2cnv  26987  log2ublem3  26991  log2ub  26992  logfacbnd3  27267  bclbnd  27324  bpos1  27327  bposlem8  27335  lgsdilem  27368  lgsdir2lem1  27369  lgsdir2lem4  27372  lgsdir2lem5  27373  lgsdir2  27374  lgsdir  27376  2lgsoddprmlem3c  27456  dchrisum0flblem1  27552  rpvmasum2  27556  log2sumbnd  27588  ax5seglem7  28950  ex-fl  30466  ipasslem10  30858  hisubcomi  31123  normlem1  31129  normlem9  31137  norm-ii-i  31156  normsubi  31160  polid2i  31176  lnophmlem2  32036  lnfn0i  32061  nmopcoi  32114  unierri  32123  addltmulALT  32465  dpmul4  32896  sgnmul  34545  logdivsqrle  34665  hgt750lem  34666  hgt750lem2  34667  problem4  35673  quad3  35675  cnndvlem1  36538  sin2h  37617  poimirlem26  37653  cntotbnd  37803  60gcd6e6  42005  12lcm5e60  42009  60lcm7e420  42011  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  sqdeccom12  42324  ex-decpmul  42340  1tiei  42352  areaquad  43228  resqrtvalex  43658  imsqrtvalex  43659  coskpi2  45881  stoweidlem13  46028  wallispilem2  46081  wallispilem4  46083  wallispi2lem1  46086  dirkerper  46111  dirkertrigeqlem1  46113  dirkercncflem1  46118  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  257prm  47548  fmtnofac1  47557  fmtno4prmfac  47559  fmtno4nprmfac193  47561  fmtno5faclem1  47566  fmtno5faclem2  47567  139prmALT  47583  127prm  47586  11t31e341  47719  2exp340mod341  47720  nfermltl8rev  47729  tgoldbach  47804