Theorem mullidi 11242

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   · cmul 11133

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulcom 11192  ax-mulass 11194  ax-distr 11195  ax-1rid 11198  ax-cnre 11201

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  00id  11413  div4p1lem1div2  12527  3halfnz  12704  crreczi  14296  fac2  14347  hashxplem  14502  sgnmul  15184  bpoly1  16143  bpoly2  16149  bpoly3  16150  bpoly4  16151  efival  16246  ef01bndlem  16278  3dvdsdec  16428  3dvds2dec  16429  odd2np1lem  16436  m1expo  16471  m1exp1  16472  nno  16478  divalglem5  16493  gcdaddmlem  16620  prmo2  17138  dec5nprm  17164  2exp8  17186  13prm  17214  23prm  17217  37prm  17219  43prm  17220  83prm  17221  139prm  17222  163prm  17223  317prm  17224  631prm  17225  1259lem2  17230  1259lem3  17231  1259lem4  17232  1259lem5  17233  2503lem1  17235  2503lem2  17236  2503lem3  17237  2503prm  17238  4001lem1  17239  4001lem2  17240  4001lem3  17241  4001lem4  17242  cnmsgnsubg  21796  iaa  26567  sin2pim  26730  cos2pim  26731  sincosq3sgn  26745  sincosq4sgn  26746  tangtx  26750  sincosq1eq  26757  sincos4thpi  26758  sincos6thpi  26761  pige3ALT  26765  abssinper  26766  ang180lem2  27055  ang180lem3  27056  1cubr  27087  asin1  27139  dvatan  27180  log2cnv  27189  log2ublem3  27193  log2ub  27194  logfacbnd3  27467  bclbnd  27524  bpos1  27527  bposlem8  27535  lgsdilem  27568  lgsdir2lem1  27569  lgsdir2lem4  27572  lgsdir2lem5  27573  lgsdir2  27574  lgsdir  27576  2lgsoddprmlem3c  27656  dchrisum0flblem1  27752  rpvmasum2  27756  log2sumbnd  27788  ax5seglem7  29400  ex-fl  30935  ipasslem10  31328  hisubcomi  31593  normlem1  31599  normlem9  31607  norm-ii-i  31626  normsubi  31630  polid2i  31646  lnophmlem2  32506  lnfn0i  32531  nmopcoi  32584  unierri  32593  addltmulALT  32935  dpmul4  33367  iconstr  34284  cos9thpiminplylem5  34304  logdivsqrle  35166  hgt750lem  35167  hgt750lem2  35168  problem4  36255  quad3  36257  cnndvlem1  37242  sin2h  38372  poimirlem26  38403  cntotbnd  38554  60gcd6e6  42878  12lcm5e60  42882  60lcm7e420  42884  3lexlogpow5ineq1  42928  3lexlogpow5ineq5  42934  sqdeccom12  43172  ex-decpmul  43189  1tiei  43200  sin2t3rdpi  43236  cos2t3rdpi  43237  areaquad  44065  resqrtvalex  44493  imsqrtvalex  44494  coskpi2  46702  stoweidlem13  46849  wallispilem2  46902  wallispilem4  46904  wallispi2lem1  46907  dirkerper  46932  dirkertrigeqlem1  46934  dirkercncflem1  46939  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  cos5t  47751  goldpolyfactor  47753  goldratval  47762  lamberte  47764  rehalfge1  48235  257prm  48472  fmtnofac1  48481  fmtno4prmfac  48483  fmtno4nprmfac193  48485  fmtno5faclem1  48490  fmtno5faclem2  48491  139prmALT  48507  127prm  48510  11t31e341  48656  2exp340mod341  48657  nfermltl8rev  48666  tgoldbach  48741