Theorem mulridi 11183

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulcom 11134  ax-mulass 11136  ax-distr 11137  ax-1rid 11140  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  addrid  11360  0lt1  11706  muleqadd  11828  1t1e1  12376  2t1e2  12377  3t1e3  12379  9p1e10  12687  numltc  12716  numsucc  12730  dec10p  12733  numadd  12737  numaddc  12738  11multnc  12758  4t3lem  12787  5t2e10  12790  9t11e99OLD  12821  nn0opthlem1  14278  faclbnd4lem1  14303  rei  15166  imi  15167  cji  15169  sqrtm1  15285  0.999...  15894  efival  16167  ef01bndlem  16199  5ndvds6  16431  3lcm2e6  16750  decsplit0b  17098  2exp8  17107  37prm  17140  43prm  17141  83prm  17142  139prm  17143  163prm  17144  317prm  17145  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  2503lem1  17156  2503lem2  17157  2503prm  17159  4001lem1  17160  4001lem2  17161  4001lem3  17162  cnmsgnsubg  21609  mdetralt  22648  dveflem  26021  dvsincos  26023  efhalfpi  26513  pige3ALT  26562  cosne0  26571  efif1olem4  26587  logf1o2  26692  asin1  26936  dvatan  26977  log2ublem3  26990  log2ub  26991  birthday  26996  basellem9  27130  ppiub  27245  chtub  27253  bposlem8  27332  lgsdir2  27371  mulog2sumlem2  27576  pntlemb  27638  avril1  30611  ipidsq  30859  nmopadjlem  32238  nmopcoadji  32250  unierri  32253  sgnmul  32987  signswch  34819  itgexpif  34864  reprlt  34877  breprexp  34891  hgt750lem  34909  hgt750lem2  34910  circum  35988  dvasin  38167  3lexlogpow5ineq1  42635  3lexlogpow5ineq5  42641  aks4d1p1  42657  235t711  42878  ex-decpmul  42879  it1ei  42889  sqrtcval2  44182  resqrtvalex  44185  imsqrtvalex  44186  inductionexd  44695  xralrple3  45913  wallispi  46608  wallispi2lem2  46610  stirlinglem1  46612  dirkertrigeqlem3  46638  modm1p1ne  47934  257prm  48134  fmtno4prmfac193  48146  fmtno5fac  48155  139prmALT  48169  127prm  48172  2exp340mod341  48319