Theorem mulridi 11340

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  addrid  11517  0lt1  11865  muleqadd  11987  1t1e1  12531  2t1e2  12532  3t1e3  12534  9p1e10  12843  numltc  12872  numsucc  12886  dec10p  12889  numadd  12893  numaddc  12894  11multnc  12914  4t3lem  12943  5t2e10  12946  9t11e99OLD  12977  nn0opthlem1  14439  faclbnd4lem1  14464  sgnmul  15289  rei  15352  imi  15353  cji  15355  sqrtm1  15471  0.999...  16079  efival  16349  ef01bndlem  16381  5ndvds6  16613  3lcm2e6  16937  decsplit0b  17286  2exp8  17295  37prm  17328  43prm  17329  83prm  17330  139prm  17331  163prm  17332  317prm  17333  1259lem1  17338  1259lem2  17339  1259lem3  17340  1259lem4  17341  1259lem5  17342  2503lem1  17344  2503lem2  17345  2503prm  17347  4001lem1  17348  4001lem2  17349  4001lem3  17350  cnmsgnsubg  21913  mdetralt  22953  dveflem  26329  dvsincos  26331  efhalfpi  26830  pige3ALT  26878  cosne0  26887  efif1olem4  26903  logf1o2  27008  asin1  27252  dvatan  27293  log2ublem3  27306  log2ub  27307  birthday  27312  basellem9  27446  ppiub  27561  chtub  27569  bposlem8  27648  lgsdir2  27687  mulog2sumlem2  27892  pntlemb  27954  avril1  31094  ipidsq  31342  nmopadjlem  32721  nmopcoadji  32733  unierri  32736  signswch  35260  itgexpif  35305  reprlt  35318  breprexp  35332  hgt750lem  35350  hgt750lem2  35351  circum  36606  dvasin  38814  3lexlogpow5ineq1  43296  3lexlogpow5ineq5  43302  aks4d1p1  43318  235t711  43555  ex-decpmul  43556  it1ei  43566  sqrtcval2  44834  resqrtvalex  44837  imsqrtvalex  44838  inductionexd  45347  xralrple3  46590  wallispi  47285  wallispi2lem2  47287  stirlinglem1  47289  dirkertrigeqlem3  47315  goldpolyfactor  48132  goldratval  48141  modm1p1ne  48651  257prm  48851  fmtno4prmfac193  48863  fmtno5fac  48872  139prmALT  48886  127prm  48889  2exp340mod341  49036