Theorem mulridi 11265

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   · cmul 11160

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 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  addrid  11441  0lt1  11785  muleqadd  11907  1t1e1  12428  2t1e2  12429  3t1e3  12431  halfpm6th  12487  9p1e10  12735  numltc  12759  numsucc  12773  dec10p  12776  numadd  12780  numaddc  12781  11multnc  12801  4t3lem  12830  5t2e10  12833  9t11e99  12863  nn0opthlem1  14307  faclbnd4lem1  14332  rei  15195  imi  15196  cji  15198  sqrtm1  15314  0.999...  15917  efival  16188  ef01bndlem  16220  5ndvds6  16451  3lcm2e6  16769  decsplit0b  17117  2exp8  17126  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  cnmsgnsubg  21595  mdetralt  22614  dveflem  26017  dvsincos  26019  efhalfpi  26513  pige3ALT  26562  cosne0  26571  efif1olem4  26587  logf1o2  26692  asin1  26937  dvatan  26978  log2ublem3  26991  log2ub  26992  birthday  26997  basellem9  27132  ppiub  27248  chtub  27256  bposlem8  27335  lgsdir2  27374  mulog2sumlem2  27579  pntlemb  27641  avril1  30482  ipidsq  30729  nmopadjlem  32108  nmopcoadji  32120  unierri  32123  sgnmul  34545  signswch  34576  itgexpif  34621  reprlt  34634  breprexp  34648  hgt750lem  34666  hgt750lem2  34667  circum  35679  dvasin  37711  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1  42077  235t711  42339  ex-decpmul  42340  it1ei  42351  sqrtcval2  43655  resqrtvalex  43658  imsqrtvalex  43659  inductionexd  44168  xralrple3  45385  wallispi  46085  wallispi2lem2  46087  stirlinglem1  46089  dirkertrigeqlem3  46115  257prm  47548  fmtno4prmfac193  47560  fmtno5fac  47569  139prmALT  47583  127prm  47586  2exp340mod341  47720