Theorem mulridi 11116

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   · cmul 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  addrid  11293  0lt1  11639  muleqadd  11761  1t1e1  12282  2t1e2  12283  3t1e3  12285  9p1e10  12590  numltc  12614  numsucc  12628  dec10p  12631  numadd  12635  numaddc  12636  11multnc  12656  4t3lem  12685  5t2e10  12688  9t11e99  12718  nn0opthlem1  14175  faclbnd4lem1  14200  rei  15063  imi  15064  cji  15066  sqrtm1  15182  0.999...  15788  efival  16061  ef01bndlem  16093  5ndvds6  16325  3lcm2e6  16643  decsplit0b  16991  2exp8  17000  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  cnmsgnsubg  21514  mdetralt  22523  dveflem  25910  dvsincos  25912  efhalfpi  26407  pige3ALT  26456  cosne0  26465  efif1olem4  26481  logf1o2  26586  asin1  26831  dvatan  26872  log2ublem3  26885  log2ub  26886  birthday  26891  basellem9  27026  ppiub  27142  chtub  27150  bposlem8  27229  lgsdir2  27268  mulog2sumlem2  27473  pntlemb  27535  avril1  30443  ipidsq  30690  nmopadjlem  32069  nmopcoadji  32081  unierri  32084  sgnmul  32818  signswch  34574  itgexpif  34619  reprlt  34632  breprexp  34646  hgt750lem  34664  hgt750lem2  34665  circum  35718  dvasin  37743  3lexlogpow5ineq1  42146  3lexlogpow5ineq5  42152  aks4d1p1  42168  235t711  42397  ex-decpmul  42398  it1ei  42408  sqrtcval2  43734  resqrtvalex  43737  imsqrtvalex  43738  inductionexd  44247  xralrple3  45471  wallispi  46167  wallispi2lem2  46169  stirlinglem1  46171  dirkertrigeqlem3  46197  modm1p1ne  47469  257prm  47660  fmtno4prmfac193  47672  fmtno5fac  47681  139prmALT  47695  127prm  47698  2exp340mod341  47832