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

Theorem mulid1i 9899
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 9894 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2ax-mp 5 1 (𝐴 · 1) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9791  1c1 9794   · cmul 9798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-mulcl 9855  ax-mulcom 9857  ax-mulass 9859  ax-distr 9860  ax-1rid 9863  ax-cnre 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  addid1  10068  0lt1  10402  muleqadd  10523  1t1e1  11025  2t1e2  11026  3t1e3  11028  halfpm6th  11103  9p1e10  11331  numltc  11363  numsucc  11384  dec10p  11388  dec10pOLD  11389  numadd  11395  numaddc  11396  11multnc  11427  4t3lem  11466  5t2e10  11469  9t11e99  11506  9t11e99OLD  11507  nn0opthlem1  12875  faclbnd4lem1  12900  rei  13693  imi  13694  cji  13696  sqrtm1  13813  0.999...  14400  0.999...OLD  14401  efival  14670  ef01bndlem  14702  3lcm2e6  15227  decsplit0b  15571  decsplit0bOLD  15575  2exp8  15583  37prm  15615  43prm  15616  83prm  15617  139prm  15618  163prm  15619  317prm  15620  1259lem1  15625  1259lem2  15626  1259lem3  15627  1259lem4  15628  1259lem5  15629  2503lem1  15631  2503lem2  15632  2503prm  15634  4001lem1  15635  4001lem2  15636  4001lem3  15637  cnmsgnsubg  19690  mdetralt  20181  dveflem  23491  dvsincos  23493  efhalfpi  23972  pige3  24018  cosne0  24025  efif1olem4  24040  logf1o2  24141  asin1  24366  dvatan  24407  log2ublem3  24420  log2ub  24421  birthday  24426  basellem9  24560  ppiub  24674  chtub  24682  bposlem8  24761  lgsdir2  24800  mulog2sumlem2  24969  pntlemb  25031  avril1  26505  ipidsq  26781  nmopadjlem  28166  nmopcoadji  28178  unierri  28181  sgnmul  29765  signswch  29798  circum  30656  dvasin  32490  inductionexd  37297  xralrple3  38355  wallispi  38787  wallispi2lem2  38789  stirlinglem1  38791  dirkertrigeqlem3  38817  257prm  39836  fmtno4prmfac193  39848  fmtno5fac  39857  139prmALT  39874  127prm  39878
  Copyright terms: Public domain W3C validator