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

Theorem mulid1i 10339
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 10333 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2ax-mp 5 1 (𝐴 · 1) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2157  (class class class)co 6884  cc 10229  1c1 10232   · cmul 10236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-mulcl 10293  ax-mulcom 10295  ax-mulass 10297  ax-distr 10298  ax-1rid 10301  ax-cnre 10304
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6074  df-fv 6119  df-ov 6887
This theorem is referenced by:  addid1  10511  0lt1  10845  muleqadd  10966  1t1e1  11481  2t1e2  11482  3t1e3  11484  halfpm6th  11540  9p1e10  11781  numltc  11805  numsucc  11819  dec10p  11822  numadd  11826  numaddc  11827  11multnc  11847  4t3lem  11876  5t2e10  11879  9t11e99  11909  nn0opthlem1  13295  faclbnd4lem1  13320  rei  14139  imi  14140  cji  14142  sqrtm1  14259  0.999...  14854  efival  15122  ef01bndlem  15154  3lcm2e6  15677  decsplit0b  16021  2exp8  16028  37prm  16059  43prm  16060  83prm  16061  139prm  16062  163prm  16063  317prm  16064  1259lem1  16069  1259lem2  16070  1259lem3  16071  1259lem4  16072  1259lem5  16073  2503lem1  16075  2503lem2  16076  2503prm  16078  4001lem1  16079  4001lem2  16080  4001lem3  16081  cnmsgnsubg  20150  mdetralt  20646  dveflem  23979  dvsincos  23981  efhalfpi  24461  pige3  24507  cosne0  24514  efif1olem4  24529  logf1o2  24633  asin1  24858  dvatan  24899  log2ublem3  24912  log2ub  24913  birthday  24918  basellem9  25052  ppiub  25166  chtub  25174  bposlem8  25253  lgsdir2  25292  mulog2sumlem2  25461  pntlemb  25523  avril1  27673  ipidsq  27916  nmopadjlem  29299  nmopcoadji  29311  unierri  29314  sgnmul  30952  signswch  30986  itgexpif  31032  reprlt  31045  breprexp  31059  hgt750lem  31077  hgt750lem2  31078  circum  31912  dvasin  33827  inductionexd  38971  xralrple3  40088  wallispi  40784  wallispi2lem2  40786  stirlinglem1  40788  dirkertrigeqlem3  40814  257prm  42066  fmtno4prmfac193  42078  fmtno5fac  42087  139prmALT  42104  127prm  42108
  Copyright terms: Public domain W3C validator