MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid1i Structured version   Visualization version   GIF version

Theorem mulid1i 10634
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
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 mulid1 10628 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2ax-mp 5 1 (𝐴 · 1) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10524  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  addid1  10809  0lt1  11151  muleqadd  11273  1t1e1  11788  2t1e2  11789  3t1e3  11791  halfpm6th  11847  9p1e10  12089  numltc  12113  numsucc  12127  dec10p  12130  numadd  12134  numaddc  12135  11multnc  12155  4t3lem  12184  5t2e10  12187  9t11e99  12217  nn0opthlem1  13618  faclbnd4lem1  13643  rei  14505  imi  14506  cji  14508  sqrtm1  14625  0.999...  15227  efival  15495  ef01bndlem  15527  3lcm2e6  16062  decsplit0b  16406  2exp8  16413  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  2503lem1  16460  2503lem2  16461  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  cnmsgnsubg  20651  mdetralt  21147  dveflem  24505  dvsincos  24507  efhalfpi  24986  pige3ALT  25034  cosne0  25041  efif1olem4  25056  logf1o2  25160  asin1  25399  dvatan  25440  log2ublem3  25454  log2ub  25455  birthday  25460  basellem9  25594  ppiub  25708  chtub  25716  bposlem8  25795  lgsdir2  25834  mulog2sumlem2  26039  pntlemb  26101  avril1  28170  ipidsq  28415  nmopadjlem  29794  nmopcoadji  29806  unierri  29809  sgnmul  31700  signswch  31731  itgexpif  31777  reprlt  31790  breprexp  31804  hgt750lem  31822  hgt750lem2  31823  circum  32815  dvasin  34860  235t711  39057  ex-decpmul  39058  inductionexd  40385  xralrple3  41522  wallispi  42236  wallispi2lem2  42238  stirlinglem1  42240  dirkertrigeqlem3  42266  257prm  43570  fmtno4prmfac193  43582  fmtno5fac  43591  139prmALT  43606  127prm  43610  2exp340mod341  43745
  Copyright terms: Public domain W3C validator