Theorem mulid1i 10645

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   · cmul 10542

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  addid1  10820  0lt1  11162  muleqadd  11284  1t1e1  11800  2t1e2  11801  3t1e3  11803  halfpm6th  11859  9p1e10  12101  numltc  12125  numsucc  12139  dec10p  12142  numadd  12146  numaddc  12147  11multnc  12167  4t3lem  12196  5t2e10  12199  9t11e99  12229  nn0opthlem1  13629  faclbnd4lem1  13654  rei  14515  imi  14516  cji  14518  sqrtm1  14635  0.999...  15237  efival  15505  ef01bndlem  15537  3lcm2e6  16072  decsplit0b  16416  2exp8  16423  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem1  16470  2503lem2  16471  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  cnmsgnsubg  20721  mdetralt  21217  dveflem  24576  dvsincos  24578  efhalfpi  25057  pige3ALT  25105  cosne0  25114  efif1olem4  25129  logf1o2  25233  asin1  25472  dvatan  25513  log2ublem3  25526  log2ub  25527  birthday  25532  basellem9  25666  ppiub  25780  chtub  25788  bposlem8  25867  lgsdir2  25906  mulog2sumlem2  26111  pntlemb  26173  avril1  28242  ipidsq  28487  nmopadjlem  29866  nmopcoadji  29878  unierri  29881  sgnmul  31800  signswch  31831  itgexpif  31877  reprlt  31890  breprexp  31904  hgt750lem  31922  hgt750lem2  31923  circum  32917  dvasin  34993  235t711  39197  ex-decpmul  39198  inductionexd  40525  xralrple3  41662  wallispi  42375  wallispi2lem2  42377  stirlinglem1  42379  dirkertrigeqlem3  42405  257prm  43743  fmtno4prmfac193  43755  fmtno5fac  43764  139prmALT  43779  127prm  43783  2exp340mod341  43918