Theorem mulridi 11138

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulridi	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulridi

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  addrid  11314  0lt1  11660  muleqadd  11782  1t1e1  12303  2t1e2  12304  3t1e3  12306  9p1e10  12611  numltc  12635  numsucc  12649  dec10p  12652  numadd  12656  numaddc  12657  11multnc  12677  4t3lem  12706  5t2e10  12709  9t11e99  12739  nn0opthlem1  14193  faclbnd4lem1  14218  rei  15081  imi  15082  cji  15084  sqrtm1  15200  0.999...  15806  efival  16079  ef01bndlem  16111  5ndvds6  16343  3lcm2e6  16661  decsplit0b  17009  2exp8  17018  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem1  17066  2503lem2  17067  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  cnmsgnsubg  21502  mdetralt  22511  dveflem  25899  dvsincos  25901  efhalfpi  26396  pige3ALT  26445  cosne0  26454  efif1olem4  26470  logf1o2  26575  asin1  26820  dvatan  26861  log2ublem3  26874  log2ub  26875  birthday  26880  basellem9  27015  ppiub  27131  chtub  27139  bposlem8  27218  lgsdir2  27257  mulog2sumlem2  27462  pntlemb  27524  avril1  30425  ipidsq  30672  nmopadjlem  32051  nmopcoadji  32063  unierri  32066  sgnmul  32793  signswch  34528  itgexpif  34573  reprlt  34586  breprexp  34600  hgt750lem  34618  hgt750lem2  34619  circum  35646  dvasin  37683  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  aks4d1p1  42049  235t711  42278  ex-decpmul  42279  it1ei  42289  sqrtcval2  43615  resqrtvalex  43618  imsqrtvalex  43619  inductionexd  44128  xralrple3  45354  wallispi  46052  wallispi2lem2  46054  stirlinglem1  46056  dirkertrigeqlem3  46082  modm1p1ne  47355  257prm  47546  fmtno4prmfac193  47558  fmtno5fac  47567  139prmALT  47581  127prm  47584  2exp340mod341  47718