Theorem mulid1i 10837

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

Syntax hints:   = wceq 1543   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727  1c1 10730   · cmul 10734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-mulcl 10791  ax-mulcom 10793  ax-mulass 10795  ax-distr 10796  ax-1rid 10799  ax-cnre 10802

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388  df-ov 7216

This theorem is referenced by:  addid1  11012  0lt1  11354  muleqadd  11476  1t1e1  11992  2t1e2  11993  3t1e3  11995  halfpm6th  12051  9p1e10  12295  numltc  12319  numsucc  12333  dec10p  12336  numadd  12340  numaddc  12341  11multnc  12361  4t3lem  12390  5t2e10  12393  9t11e99  12423  nn0opthlem1  13834  faclbnd4lem1  13859  rei  14719  imi  14720  cji  14722  sqrtm1  14839  0.999...  15445  efival  15713  ef01bndlem  15745  3lcm2e6  16288  decsplit0b  16633  2exp8  16642  37prm  16674  43prm  16675  83prm  16676  139prm  16677  163prm  16678  317prm  16679  1259lem1  16684  1259lem2  16685  1259lem3  16686  1259lem4  16687  1259lem5  16688  2503lem1  16690  2503lem2  16691  2503prm  16693  4001lem1  16694  4001lem2  16695  4001lem3  16696  cnmsgnsubg  20539  mdetralt  21505  dveflem  24876  dvsincos  24878  efhalfpi  25361  pige3ALT  25409  cosne0  25418  efif1olem4  25434  logf1o2  25538  asin1  25777  dvatan  25818  log2ublem3  25831  log2ub  25832  birthday  25837  basellem9  25971  ppiub  26085  chtub  26093  bposlem8  26172  lgsdir2  26211  mulog2sumlem2  26416  pntlemb  26478  avril1  28546  ipidsq  28791  nmopadjlem  30170  nmopcoadji  30182  unierri  30185  sgnmul  32221  signswch  32252  itgexpif  32298  reprlt  32311  breprexp  32325  hgt750lem  32343  hgt750lem2  32344  circum  33345  dvasin  35598  3lexlogpow5ineq1  39796  3lexlogpow5ineq5  39802  aks4d1p1  39817  235t711  40026  ex-decpmul  40027  sqrtcval2  40926  resqrtvalex  40929  imsqrtvalex  40930  inductionexd  41442  xralrple3  42586  wallispi  43286  wallispi2lem2  43288  stirlinglem1  43290  dirkertrigeqlem3  43316  257prm  44686  fmtno4prmfac193  44698  fmtno5fac  44707  139prmALT  44721  127prm  44724  2exp340mod341  44858