Theorem mulid1i 10234

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

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulid1 10229	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

Syntax hints:   = wceq 1632   ∈ wcel 2139  (class class class)co 6813  ℂcc 10126  1c1 10129   · cmul 10133

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 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-mulcl 10190  ax-mulcom 10192  ax-mulass 10194  ax-distr 10195  ax-1rid 10198  ax-cnre 10201

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 6816

This theorem is referenced by:  addid1  10408  0lt1  10742  muleqadd  10863  1t1e1  11367  2t1e2  11368  3t1e3  11370  halfpm6th  11445  9p1e10  11688  numltc  11720  numsucc  11741  dec10p  11745  dec10pOLD  11746  numadd  11752  numaddc  11753  11multnc  11784  4t3lem  11823  5t2e10  11826  9t11e99  11863  9t11e99OLD  11864  nn0opthlem1  13249  faclbnd4lem1  13274  rei  14095  imi  14096  cji  14098  sqrtm1  14215  0.999...  14811  0.999...OLD  14812  efival  15081  ef01bndlem  15113  3lcm2e6  15642  decsplit0b  15986  decsplit0bOLD  15990  2exp8  15998  37prm  16030  43prm  16031  83prm  16032  139prm  16033  163prm  16034  317prm  16035  1259lem1  16040  1259lem2  16041  1259lem3  16042  1259lem4  16043  1259lem5  16044  2503lem1  16046  2503lem2  16047  2503prm  16049  4001lem1  16050  4001lem2  16051  4001lem3  16052  cnmsgnsubg  20125  mdetralt  20616  dveflem  23941  dvsincos  23943  efhalfpi  24422  pige3  24468  cosne0  24475  efif1olem4  24490  logf1o2  24595  asin1  24820  dvatan  24861  log2ublem3  24874  log2ub  24875  birthday  24880  basellem9  25014  ppiub  25128  chtub  25136  bposlem8  25215  lgsdir2  25254  mulog2sumlem2  25423  pntlemb  25485  avril1  27630  ipidsq  27874  nmopadjlem  29257  nmopcoadji  29269  unierri  29272  sgnmul  30913  signswch  30947  itgexpif  30993  reprlt  31006  breprexp  31020  hgt750lem  31038  hgt750lem2  31039  circum  31875  dvasin  33809  inductionexd  38955  xralrple3  40088  wallispi  40790  wallispi2lem2  40792  stirlinglem1  40794  dirkertrigeqlem3  40820  257prm  41983  fmtno4prmfac193  41995  fmtno5fac  42004  139prmALT  42021  127prm  42025