Theorem mulridi 11217

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  addrid  11393  0lt1  11735  muleqadd  11857  1t1e1  12373  2t1e2  12374  3t1e3  12376  halfpm6th  12432  9p1e10  12678  numltc  12702  numsucc  12716  dec10p  12719  numadd  12723  numaddc  12724  11multnc  12744  4t3lem  12773  5t2e10  12776  9t11e99  12806  nn0opthlem1  14227  faclbnd4lem1  14252  rei  15102  imi  15103  cji  15105  sqrtm1  15221  0.999...  15826  efival  16094  ef01bndlem  16126  3lcm2e6  16667  decsplit0b  17012  2exp8  17021  37prm  17053  43prm  17054  83prm  17055  139prm  17056  163prm  17057  317prm  17058  1259lem1  17063  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  2503lem1  17069  2503lem2  17070  2503prm  17072  4001lem1  17073  4001lem2  17074  4001lem3  17075  cnmsgnsubg  21129  mdetralt  22109  dveflem  25495  dvsincos  25497  efhalfpi  25980  pige3ALT  26028  cosne0  26037  efif1olem4  26053  logf1o2  26157  asin1  26396  dvatan  26437  log2ublem3  26450  log2ub  26451  birthday  26456  basellem9  26590  ppiub  26704  chtub  26712  bposlem8  26791  lgsdir2  26830  mulog2sumlem2  27035  pntlemb  27097  avril1  29713  ipidsq  29958  nmopadjlem  31337  nmopcoadji  31349  unierri  31352  sgnmul  33536  signswch  33567  itgexpif  33613  reprlt  33626  breprexp  33640  hgt750lem  33658  hgt750lem2  33659  circum  34654  dvasin  36567  3lexlogpow5ineq1  40914  3lexlogpow5ineq5  40920  aks4d1p1  40936  235t711  41205  ex-decpmul  41206  sqrtcval2  42383  resqrtvalex  42386  imsqrtvalex  42387  inductionexd  42896  xralrple3  44074  wallispi  44776  wallispi2lem2  44778  stirlinglem1  44780  dirkertrigeqlem3  44806  257prm  46219  fmtno4prmfac193  46231  fmtno5fac  46240  139prmALT  46254  127prm  46257  2exp340mod341  46391