Theorem mullidi 11341

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  00id  11512  div4p1lem1div2  12628  3halfnz  12805  crreczi  14399  fac2  14450  hashxplem  14605  sgnmul  15289  bpoly1  16246  bpoly2  16252  bpoly3  16253  bpoly4  16254  efival  16349  ef01bndlem  16381  3dvdsdec  16531  3dvds2dec  16532  odd2np1lem  16539  m1expo  16574  m1exp1  16575  nno  16581  divalglem5  16596  gcdaddmlem  16725  prmo2  17247  dec5nprm  17273  2exp8  17295  13prm  17323  23prm  17326  37prm  17328  43prm  17329  83prm  17330  139prm  17331  163prm  17332  317prm  17333  631prm  17334  1259lem2  17339  1259lem3  17340  1259lem4  17341  1259lem5  17342  2503lem1  17344  2503lem2  17345  2503lem3  17346  2503prm  17347  4001lem1  17348  4001lem2  17349  4001lem3  17350  4001lem4  17351  cnmsgnsubg  21913  iaa  26681  sin2pim  26844  cos2pim  26845  sincosq3sgn  26859  sincosq4sgn  26860  tangtx  26864  sincosq1eq  26871  sincos4thpi  26872  sincos6thpi  26874  pige3ALT  26878  abssinper  26879  ang180lem2  27168  ang180lem3  27169  1cubr  27200  asin1  27252  dvatan  27293  log2cnv  27302  log2ublem3  27306  log2ub  27307  logfacbnd3  27580  bclbnd  27637  bpos1  27640  bposlem8  27648  lgsdilem  27681  lgsdir2lem1  27682  lgsdir2lem4  27685  lgsdir2lem5  27686  lgsdir2  27687  lgsdir  27689  2lgsoddprmlem3c  27769  dchrisum0flblem1  27865  rpvmasum2  27869  log2sumbnd  27901  ax5seglem7  29543  ex-fl  31078  ipasslem10  31471  hisubcomi  31736  normlem1  31742  normlem9  31750  norm-ii-i  31769  normsubi  31773  polid2i  31789  lnophmlem2  32649  lnfn0i  32674  nmopcoi  32727  unierri  32736  addltmulALT  33120  dpmul4  33550  iconstr  34468  cos9thpiminplylem5  34488  logdivsqrle  35349  hgt750lem  35350  hgt750lem2  35351  problem4  36600  quad3  36602  cnndvlem1  37581  sin2h  38725  poimirlem26  38756  cntotbnd  38922  60gcd6e6  43246  12lcm5e60  43250  60lcm7e420  43252  3lexlogpow5ineq1  43296  3lexlogpow5ineq5  43302  sqdeccom12  43539  ex-decpmul  43556  1tiei  43567  sin2t3rdpi  43597  cos2t3rdpi  43598  areaquad  44410  resqrtvalex  44837  imsqrtvalex  44838  coskpi2  47081  stoweidlem13  47228  wallispilem2  47281  wallispilem4  47283  wallispi2lem1  47286  dirkerper  47311  dirkertrigeqlem1  47313  dirkercncflem1  47318  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  cos5t  48130  goldpolyfactor  48132  goldratval  48141  lamberte  48143  rehalfge1  48614  257prm  48851  fmtnofac1  48860  fmtno4prmfac  48862  fmtno4nprmfac193  48864  fmtno5faclem1  48869  fmtno5faclem2  48870  139prmALT  48886  127prm  48889  11t31e341  49035  2exp340mod341  49036  nfermltl8rev  49045  tgoldbach  49120