Theorem mulid1i 10494

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 10488	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

Syntax hints:   = wceq 1522   ∈ wcel 2080  (class class class)co 7019  ℂcc 10384  1c1 10387   · cmul 10391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-mulcl 10448  ax-mulcom 10450  ax-mulass 10452  ax-distr 10453  ax-1rid 10456  ax-cnre 10459

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-br 4965  df-iota 6192  df-fv 6236  df-ov 7022

This theorem is referenced by:  addid1  10669  0lt1  11012  muleqadd  11134  1t1e1  11649  2t1e2  11650  3t1e3  11652  halfpm6th  11708  9p1e10  11950  numltc  11974  numsucc  11988  dec10p  11991  numadd  11995  numaddc  11996  11multnc  12016  4t3lem  12045  5t2e10  12048  9t11e99  12078  nn0opthlem1  13478  faclbnd4lem1  13503  rei  14349  imi  14350  cji  14352  sqrtm1  14469  0.999...  15070  efival  15338  ef01bndlem  15370  3lcm2e6  15901  decsplit0b  16245  2exp8  16252  37prm  16283  43prm  16284  83prm  16285  139prm  16286  163prm  16287  317prm  16288  1259lem1  16293  1259lem2  16294  1259lem3  16295  1259lem4  16296  1259lem5  16297  2503lem1  16299  2503lem2  16300  2503prm  16302  4001lem1  16303  4001lem2  16304  4001lem3  16305  cnmsgnsubg  20403  mdetralt  20901  dveflem  24259  dvsincos  24261  efhalfpi  24740  pige3ALT  24788  cosne0  24795  efif1olem4  24810  logf1o2  24914  asin1  25153  dvatan  25194  log2ublem3  25208  log2ub  25209  birthday  25214  basellem9  25348  ppiub  25462  chtub  25470  bposlem8  25549  lgsdir2  25588  mulog2sumlem2  25793  pntlemb  25855  avril1  27925  ipidsq  28170  nmopadjlem  29549  nmopcoadji  29561  unierri  29564  sgnmul  31409  signswch  31440  itgexpif  31486  reprlt  31499  breprexp  31513  hgt750lem  31531  hgt750lem2  31532  circum  32519  dvasin  34522  235t711  38712  ex-decpmul  38713  inductionexd  40003  xralrple3  41196  wallispi  41911  wallispi2lem2  41913  stirlinglem1  41915  dirkertrigeqlem3  41941  257prm  43219  fmtno4prmfac193  43231  fmtno5fac  43240  139prmALT  43255  127prm  43259  2exp340mod341  43394