Theorem mulridi 11148

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   · cmul 11043

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  addrid  11325  0lt1  11671  muleqadd  11793  1t1e1  12314  2t1e2  12315  3t1e3  12317  9p1e10  12621  numltc  12645  numsucc  12659  dec10p  12662  numadd  12666  numaddc  12667  11multnc  12687  4t3lem  12716  5t2e10  12719  9t11e99  12749  nn0opthlem1  14203  faclbnd4lem1  14228  rei  15091  imi  15092  cji  15094  sqrtm1  15210  0.999...  15816  efival  16089  ef01bndlem  16121  5ndvds6  16353  3lcm2e6  16671  decsplit0b  17019  2exp8  17028  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  cnmsgnsubg  21544  mdetralt  22564  dveflem  25951  dvsincos  25953  efhalfpi  26448  pige3ALT  26497  cosne0  26506  efif1olem4  26522  logf1o2  26627  asin1  26872  dvatan  26913  log2ublem3  26926  log2ub  26927  birthday  26932  basellem9  27067  ppiub  27183  chtub  27191  bposlem8  27270  lgsdir2  27309  mulog2sumlem2  27514  pntlemb  27576  avril1  30550  ipidsq  30797  nmopadjlem  32176  nmopcoadji  32188  unierri  32191  sgnmul  32926  signswch  34738  itgexpif  34783  reprlt  34796  breprexp  34810  hgt750lem  34828  hgt750lem2  34829  circum  35887  dvasin  37949  3lexlogpow5ineq1  42418  3lexlogpow5ineq5  42424  aks4d1p1  42440  235t711  42669  ex-decpmul  42670  it1ei  42680  sqrtcval2  43992  resqrtvalex  43995  imsqrtvalex  43996  inductionexd  44505  xralrple3  45726  wallispi  46422  wallispi2lem2  46424  stirlinglem1  46426  dirkertrigeqlem3  46452  modm1p1ne  47724  257prm  47915  fmtno4prmfac193  47927  fmtno5fac  47936  139prmALT  47950  127prm  47953  2exp340mod341  48087