Theorem mullidi 11215

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulcom 11165  ax-mulass 11167  ax-distr 11168  ax-1rid 11171  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  00id  11386  div4p1lem1div2  12500  3halfnz  12676  crreczi  14266  fac2  14317  hashxplem  14472  sgnmul  15146  bpoly1  16106  bpoly2  16112  bpoly3  16113  bpoly4  16114  efival  16209  ef01bndlem  16241  3dvdsdec  16391  3dvds2dec  16392  odd2np1lem  16399  m1expo  16434  m1exp1  16435  nno  16441  divalglem5  16456  gcdaddmlem  16583  prmo2  17101  dec5nprm  17127  2exp8  17149  13prm  17177  23prm  17180  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  2503lem1  17198  2503lem2  17199  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  cnmsgnsubg  21708  sin2pim  26628  cos2pim  26629  sincosq3sgn  26643  sincosq4sgn  26644  tangtx  26648  sincosq1eq  26655  sincos4thpi  26656  sincos6thpi  26659  pige3ALT  26663  abssinper  26664  ang180lem2  26953  ang180lem3  26954  1cubr  26985  asin1  27037  dvatan  27078  log2cnv  27087  log2ublem3  27091  log2ub  27092  logfacbnd3  27365  bclbnd  27422  bpos1  27425  bposlem8  27433  lgsdilem  27466  lgsdir2lem1  27467  lgsdir2lem4  27470  lgsdir2lem5  27471  lgsdir2  27472  lgsdir  27474  2lgsoddprmlem3c  27554  dchrisum0flblem1  27650  rpvmasum2  27654  log2sumbnd  27686  ax5seglem7  29263  ex-fl  30776  ipasslem10  31169  hisubcomi  31434  normlem1  31440  normlem9  31448  norm-ii-i  31467  normsubi  31471  polid2i  31487  lnophmlem2  32347  lnfn0i  32372  nmopcoi  32425  unierri  32434  addltmulALT  32776  dpmul4  33211  iconstr  34134  cos9thpiminplylem5  34154  logdivsqrle  35015  hgt750lem  35016  hgt750lem2  35017  problem4  36138  quad3  36140  cnndvlem1  37104  sin2h  38239  poimirlem26  38275  cntotbnd  38425  60gcd6e6  42749  12lcm5e60  42753  60lcm7e420  42755  3lexlogpow5ineq1  42799  3lexlogpow5ineq5  42805  sqdeccom12  43028  ex-decpmul  43045  1tiei  43056  sin2t3rdpi  43092  cos2t3rdpi  43093  areaquad  43923  resqrtvalex  44351  imsqrtvalex  44352  coskpi2  46560  stoweidlem13  46707  wallispilem2  46760  wallispilem4  46762  wallispi2lem1  46765  dirkerper  46790  dirkertrigeqlem1  46792  dirkercncflem1  46797  sqwvfoura  46922  sqwvfourb  46923  fourierswlem  46924  fouriersw  46925  cos5t  47593  lamberte  47602  rehalfge1  48053  257prm  48290  fmtnofac1  48299  fmtno4prmfac  48301  fmtno4nprmfac193  48303  fmtno5faclem1  48308  fmtno5faclem2  48309  139prmALT  48325  127prm  48328  11t31e341  48474  2exp340mod341  48475  nfermltl8rev  48484  tgoldbach  48559