Theorem mulridi 11237

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   · cmul 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  addrid  11413  0lt1  11757  muleqadd  11879  1t1e1  12400  2t1e2  12401  3t1e3  12403  9p1e10  12708  numltc  12732  numsucc  12746  dec10p  12749  numadd  12753  numaddc  12754  11multnc  12774  4t3lem  12803  5t2e10  12806  9t11e99  12836  nn0opthlem1  14284  faclbnd4lem1  14309  rei  15173  imi  15174  cji  15176  sqrtm1  15292  0.999...  15895  efival  16168  ef01bndlem  16200  5ndvds6  16431  3lcm2e6  16749  decsplit0b  17097  2exp8  17106  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  cnmsgnsubg  21535  mdetralt  22544  dveflem  25933  dvsincos  25935  efhalfpi  26430  pige3ALT  26479  cosne0  26488  efif1olem4  26504  logf1o2  26609  asin1  26854  dvatan  26895  log2ublem3  26908  log2ub  26909  birthday  26914  basellem9  27049  ppiub  27165  chtub  27173  bposlem8  27252  lgsdir2  27291  mulog2sumlem2  27496  pntlemb  27558  avril1  30390  ipidsq  30637  nmopadjlem  32016  nmopcoadji  32028  unierri  32031  sgnmul  32760  signswch  34539  itgexpif  34584  reprlt  34597  breprexp  34611  hgt750lem  34629  hgt750lem2  34630  circum  35642  dvasin  37674  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  aks4d1p1  42035  235t711  42301  ex-decpmul  42302  it1ei  42312  sqrtcval2  43613  resqrtvalex  43616  imsqrtvalex  43617  inductionexd  44126  xralrple3  45349  wallispi  46047  wallispi2lem2  46049  stirlinglem1  46051  dirkertrigeqlem3  46077  257prm  47523  fmtno4prmfac193  47535  fmtno5fac  47544  139prmALT  47558  127prm  47561  2exp340mod341  47695