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

Theorem mulid1i 8839
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
axi.1  |-  A  e.  CC
Assertion
Ref Expression
mulid1i  |-  ( A  x.  1 )  =  A

Proof of Theorem mulid1i
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 mulid1 8835 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
31, 2ax-mp 8 1  |-  ( A  x.  1 )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735   1c1 8738    x. cmul 8742
This theorem is referenced by:  addid1  8992  0lt1  9296  muleqadd  9412  1t1e1  9870  3t3e9  9873  halfpm6th  9936  numltc  10144  numsucc  10150  dec10p  10153  numadd  10158  numaddc  10159  4t3lem  10195  decbin2  10228  expubnd  11162  nn0opthlem1  11283  faclbnd4lem1  11306  rei  11641  imi  11642  cji  11644  sqrm1  11761  trirecip  12321  0.999...  12337  ege2le3  12371  efival  12432  cos2tsin  12459  ef01bndlem  12464  cos2bnd  12468  odd2np1  12587  opoe  12864  pythagtriplem4  12872  decsplit0b  13095  2exp8  13102  5prm  13110  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  htpycc  18478  pco1  18513  pcohtpylem  18517  pcopt  18520  pcorevlem  18524  ovolunlem1a  18855  dveflem  19326  dvsincos  19328  efhalfpi  19839  cos2pi  19844  pige3  19885  coskpi  19888  cosne0  19892  efif1olem4  19907  logf1o2  19997  dcubic1lem  20139  dcubic2  20140  dcubic  20142  mcubic  20143  asin1  20190  dvatan  20231  log2ublem3  20244  log2ub  20245  birthday  20249  basellem3  20320  basellem9  20326  ppiub  20443  chtublem  20450  chtub  20451  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  bposlem2  20524  bposlem5  20527  bposlem8  20530  lgsdir2  20567  chebbnd1lem1  20618  chebbnd1lem3  20620  chebbnd1  20621  mulog2sumlem2  20684  pntlemb  20746  avril1  20836  ipidsq  21286  nmopadjlem  22669  nmopcoadji  22681  unierri  22684  konigsberg  23322  circum  23418  bpoly3  24204  fsumcube  24206  dvreasin  24334  heiborlem6  25952  jm2.23  26501  cnmsgnsubg  26846  lhe4.4ex1a  26958  stoweidlem51  27212  wallispilem4  27229  wallispi  27231  wallispi2lem1  27232  wallispi2lem2  27233  wallispi2  27234  stirlinglem1  27235  stirlinglem11  27245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator