Theorem mulid1i 11052

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulid1i	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulid1i

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulid1 11046	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7315  ℂcc 10942  1c1 10945   · cmul 10949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-mulcl 11006  ax-mulcom 11008  ax-mulass 11010  ax-distr 11011  ax-1rid 11014  ax-cnre 11017

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-iota 6417  df-fv 6473  df-ov 7318

This theorem is referenced by:  addid1  11228  0lt1  11570  muleqadd  11692  1t1e1  12208  2t1e2  12209  3t1e3  12211  halfpm6th  12267  9p1e10  12512  numltc  12536  numsucc  12550  dec10p  12553  numadd  12557  numaddc  12558  11multnc  12578  4t3lem  12607  5t2e10  12610  9t11e99  12640  nn0opthlem1  14055  faclbnd4lem1  14080  rei  14939  imi  14940  cji  14942  sqrtm1  15059  0.999...  15665  efival  15933  ef01bndlem  15965  3lcm2e6  16506  decsplit0b  16851  2exp8  16860  37prm  16892  43prm  16893  83prm  16894  139prm  16895  163prm  16896  317prm  16897  1259lem1  16902  1259lem2  16903  1259lem3  16904  1259lem4  16905  1259lem5  16906  2503lem1  16908  2503lem2  16909  2503prm  16911  4001lem1  16912  4001lem2  16913  4001lem3  16914  cnmsgnsubg  20854  mdetralt  21829  dveflem  25215  dvsincos  25217  efhalfpi  25700  pige3ALT  25748  cosne0  25757  efif1olem4  25773  logf1o2  25877  asin1  26116  dvatan  26157  log2ublem3  26170  log2ub  26171  birthday  26176  basellem9  26310  ppiub  26424  chtub  26432  bposlem8  26511  lgsdir2  26550  mulog2sumlem2  26755  pntlemb  26817  avril1  28936  ipidsq  29181  nmopadjlem  30560  nmopcoadji  30572  unierri  30575  sgnmul  32615  signswch  32646  itgexpif  32692  reprlt  32705  breprexp  32719  hgt750lem  32737  hgt750lem2  32738  circum  33737  dvasin  35917  3lexlogpow5ineq1  40267  3lexlogpow5ineq5  40273  aks4d1p1  40289  235t711  40522  ex-decpmul  40523  sqrtcval2  41471  resqrtvalex  41474  imsqrtvalex  41475  inductionexd  41986  xralrple3  43149  wallispi  43848  wallispi2lem2  43850  stirlinglem1  43852  dirkertrigeqlem3  43878  257prm  45265  fmtno4prmfac193  45277  fmtno5fac  45286  139prmALT  45300  127prm  45303  2exp340mod341  45437