Theorem mulridi 11140

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  addrid  11317  0lt1  11663  muleqadd  11785  1t1e1  12329  2t1e2  12330  3t1e3  12332  9p1e10  12637  numltc  12661  numsucc  12675  dec10p  12678  numadd  12682  numaddc  12683  11multnc  12703  4t3lem  12732  5t2e10  12735  9t11e99  12765  nn0opthlem1  14221  faclbnd4lem1  14246  rei  15109  imi  15110  cji  15112  sqrtm1  15228  0.999...  15837  efival  16110  ef01bndlem  16142  5ndvds6  16374  3lcm2e6  16693  decsplit0b  17041  2exp8  17050  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  cnmsgnsubg  21567  mdetralt  22583  dveflem  25956  dvsincos  25958  efhalfpi  26448  pige3ALT  26497  cosne0  26506  efif1olem4  26522  logf1o2  26627  asin1  26871  dvatan  26912  log2ublem3  26925  log2ub  26926  birthday  26931  basellem9  27066  ppiub  27181  chtub  27189  bposlem8  27268  lgsdir2  27307  mulog2sumlem2  27512  pntlemb  27574  avril1  30548  ipidsq  30796  nmopadjlem  32175  nmopcoadji  32187  unierri  32190  sgnmul  32923  signswch  34721  itgexpif  34766  reprlt  34779  breprexp  34793  hgt750lem  34811  hgt750lem2  34812  circum  35872  dvasin  38039  3lexlogpow5ineq1  42507  3lexlogpow5ineq5  42513  aks4d1p1  42529  235t711  42751  ex-decpmul  42752  it1ei  42762  sqrtcval2  44087  resqrtvalex  44090  imsqrtvalex  44091  inductionexd  44600  xralrple3  45821  wallispi  46516  wallispi2lem2  46518  stirlinglem1  46520  dirkertrigeqlem3  46546  modm1p1ne  47836  257prm  48036  fmtno4prmfac193  48048  fmtno5fac  48057  139prmALT  48071  127prm  48074  2exp340mod341  48221