Theorem mulridi 11201

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-mulcom 11152  ax-mulass 11154  ax-distr 11155  ax-1rid 11158  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  addrid  11378  0lt1  11724  muleqadd  11846  1t1e1  12393  2t1e2  12394  3t1e3  12396  9p1e10  12704  numltc  12733  numsucc  12747  dec10p  12750  numadd  12754  numaddc  12755  11multnc  12775  4t3lem  12804  5t2e10  12807  9t11e99OLD  12838  nn0opthlem1  14295  faclbnd4lem1  14320  sgnmul  15134  rei  15197  imi  15198  cji  15200  sqrtm1  15316  0.999...  15925  efival  16198  ef01bndlem  16230  5ndvds6  16462  3lcm2e6  16781  decsplit0b  17129  2exp8  17138  37prm  17171  43prm  17172  83prm  17173  139prm  17174  163prm  17175  317prm  17176  1259lem1  17181  1259lem2  17182  1259lem3  17183  1259lem4  17184  1259lem5  17185  2503lem1  17187  2503lem2  17188  2503prm  17190  4001lem1  17191  4001lem2  17192  4001lem3  17193  cnmsgnsubg  21687  mdetralt  22726  dveflem  26099  dvsincos  26101  efhalfpi  26594  pige3ALT  26643  cosne0  26652  efif1olem4  26668  logf1o2  26773  asin1  27017  dvatan  27058  log2ublem3  27071  log2ub  27072  birthday  27077  basellem9  27211  ppiub  27326  chtub  27334  bposlem8  27413  lgsdir2  27452  mulog2sumlem2  27657  pntlemb  27719  avril1  30723  ipidsq  30971  nmopadjlem  32350  nmopcoadji  32362  unierri  32365  signswch  34865  itgexpif  34910  reprlt  34923  breprexp  34937  hgt750lem  34955  hgt750lem2  34956  circum  36037  dvasin  38215  3lexlogpow5ineq1  42683  3lexlogpow5ineq5  42689  aks4d1p1  42705  235t711  42926  ex-decpmul  42927  it1ei  42937  sqrtcval2  44230  resqrtvalex  44233  imsqrtvalex  44234  inductionexd  44743  xralrple3  45947  wallispi  46642  wallispi2lem2  46644  stirlinglem1  46646  dirkertrigeqlem3  46672  modm1p1ne  47968  257prm  48168  fmtno4prmfac193  48180  fmtno5fac  48189  139prmALT  48203  127prm  48206  2exp340mod341  48353