Theorem mulridi 11223

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11112  1c1 11115   · cmul 11119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-mulcl 11176  ax-mulcom 11178  ax-mulass 11180  ax-distr 11181  ax-1rid 11184  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3432  df-v 3475  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 7415

This theorem is referenced by:  addrid  11399  0lt1  11741  muleqadd  11863  1t1e1  12379  2t1e2  12380  3t1e3  12382  halfpm6th  12438  9p1e10  12684  numltc  12708  numsucc  12722  dec10p  12725  numadd  12729  numaddc  12730  11multnc  12750  4t3lem  12779  5t2e10  12782  9t11e99  12812  nn0opthlem1  14233  faclbnd4lem1  14258  rei  15108  imi  15109  cji  15111  sqrtm1  15227  0.999...  15832  efival  16100  ef01bndlem  16132  3lcm2e6  16673  decsplit0b  17018  2exp8  17027  37prm  17059  43prm  17060  83prm  17061  139prm  17062  163prm  17063  317prm  17064  1259lem1  17069  1259lem2  17070  1259lem3  17071  1259lem4  17072  1259lem5  17073  2503lem1  17075  2503lem2  17076  2503prm  17078  4001lem1  17079  4001lem2  17080  4001lem3  17081  cnmsgnsubg  21350  mdetralt  22331  dveflem  25732  dvsincos  25734  efhalfpi  26218  pige3ALT  26266  cosne0  26275  efif1olem4  26291  logf1o2  26395  asin1  26636  dvatan  26677  log2ublem3  26690  log2ub  26691  birthday  26696  basellem9  26830  ppiub  26944  chtub  26952  bposlem8  27031  lgsdir2  27070  mulog2sumlem2  27275  pntlemb  27337  avril1  29984  ipidsq  30231  nmopadjlem  31610  nmopcoadji  31622  unierri  31625  sgnmul  33840  signswch  33871  itgexpif  33917  reprlt  33930  breprexp  33944  hgt750lem  33962  hgt750lem2  33963  circum  34958  dvasin  36876  3lexlogpow5ineq1  41226  3lexlogpow5ineq5  41232  aks4d1p1  41248  235t711  41508  ex-decpmul  41509  sqrtcval2  42696  resqrtvalex  42699  imsqrtvalex  42700  inductionexd  43209  xralrple3  44383  wallispi  45085  wallispi2lem2  45087  stirlinglem1  45089  dirkertrigeqlem3  45115  257prm  46528  fmtno4prmfac193  46540  fmtno5fac  46549  139prmALT  46563  127prm  46566  2exp340mod341  46700