Theorem mulridi 11214

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulcom 11165  ax-mulass 11167  ax-distr 11168  ax-1rid 11171  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  addrid  11391  0lt1  11737  muleqadd  11859  1t1e1  12403  2t1e2  12404  3t1e3  12406  9p1e10  12714  numltc  12743  numsucc  12757  dec10p  12760  numadd  12764  numaddc  12765  11multnc  12785  4t3lem  12814  5t2e10  12817  9t11e99OLD  12848  nn0opthlem1  14306  faclbnd4lem1  14331  sgnmul  15146  rei  15209  imi  15210  cji  15212  sqrtm1  15328  0.999...  15937  efival  16209  ef01bndlem  16241  5ndvds6  16473  3lcm2e6  16792  decsplit0b  17140  2exp8  17149  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  2503lem1  17198  2503lem2  17199  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  cnmsgnsubg  21708  mdetralt  22746  dveflem  26119  dvsincos  26121  efhalfpi  26614  pige3ALT  26663  cosne0  26672  efif1olem4  26688  logf1o2  26793  asin1  27037  dvatan  27078  log2ublem3  27091  log2ub  27092  birthday  27097  basellem9  27231  ppiub  27346  chtub  27354  bposlem8  27433  lgsdir2  27472  mulog2sumlem2  27677  pntlemb  27739  avril1  30792  ipidsq  31040  nmopadjlem  32419  nmopcoadji  32431  unierri  32434  signswch  34926  itgexpif  34971  reprlt  34984  breprexp  34998  hgt750lem  35016  hgt750lem2  35017  circum  36144  dvasin  38333  3lexlogpow5ineq1  42799  3lexlogpow5ineq5  42805  aks4d1p1  42821  235t711  43044  ex-decpmul  43045  it1ei  43055  sqrtcval2  44348  resqrtvalex  44351  imsqrtvalex  44352  inductionexd  44861  xralrple3  46069  wallispi  46764  wallispi2lem2  46766  stirlinglem1  46768  dirkertrigeqlem3  46794  modm1p1ne  48090  257prm  48290  fmtno4prmfac193  48302  fmtno5fac  48311  139prmALT  48325  127prm  48328  2exp340mod341  48475