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

Theorem mulid1i 10254
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 10249 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2ax-mp 5 1 (𝐴 · 1) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  (class class class)co 6814  cc 10146  1c1 10149   · cmul 10153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-mulcl 10210  ax-mulcom 10212  ax-mulass 10214  ax-distr 10215  ax-1rid 10218  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817
This theorem is referenced by:  addid1  10428  0lt1  10762  muleqadd  10883  1t1e1  11387  2t1e2  11388  3t1e3  11390  halfpm6th  11465  9p1e10  11708  numltc  11740  numsucc  11761  dec10p  11765  dec10pOLD  11766  numadd  11772  numaddc  11773  11multnc  11804  4t3lem  11843  5t2e10  11846  9t11e99  11883  9t11e99OLD  11884  nn0opthlem1  13269  faclbnd4lem1  13294  rei  14115  imi  14116  cji  14118  sqrtm1  14235  0.999...  14831  0.999...OLD  14832  efival  15101  ef01bndlem  15133  3lcm2e6  15662  decsplit0b  16006  decsplit0bOLD  16010  2exp8  16018  37prm  16050  43prm  16051  83prm  16052  139prm  16053  163prm  16054  317prm  16055  1259lem1  16060  1259lem2  16061  1259lem3  16062  1259lem4  16063  1259lem5  16064  2503lem1  16066  2503lem2  16067  2503prm  16069  4001lem1  16070  4001lem2  16071  4001lem3  16072  cnmsgnsubg  20145  mdetralt  20636  dveflem  23961  dvsincos  23963  efhalfpi  24443  pige3  24489  cosne0  24496  efif1olem4  24511  logf1o2  24616  asin1  24841  dvatan  24882  log2ublem3  24895  log2ub  24896  birthday  24901  basellem9  25035  ppiub  25149  chtub  25157  bposlem8  25236  lgsdir2  25275  mulog2sumlem2  25444  pntlemb  25506  avril1  27651  ipidsq  27895  nmopadjlem  29278  nmopcoadji  29290  unierri  29293  sgnmul  30934  signswch  30968  itgexpif  31014  reprlt  31027  breprexp  31041  hgt750lem  31059  hgt750lem2  31060  circum  31896  dvasin  33827  inductionexd  38973  xralrple3  40106  wallispi  40808  wallispi2lem2  40810  stirlinglem1  40812  dirkertrigeqlem3  40838  257prm  42001  fmtno4prmfac193  42013  fmtno5fac  42022  139prmALT  42039  127prm  42043
  Copyright terms: Public domain W3C validator