Theorem mulridi 11294

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulcom 11245  ax-mulass 11247  ax-distr 11248  ax-1rid 11251  ax-cnre 11254

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  addrid  11471  0lt1  11819  muleqadd  11941  1t1e1  12485  2t1e2  12486  3t1e3  12488  9p1e10  12797  numltc  12826  numsucc  12840  dec10p  12843  numadd  12847  numaddc  12848  11multnc  12868  4t3lem  12897  5t2e10  12900  9t11e99OLD  12931  nn0opthlem1  14392  faclbnd4lem1  14417  sgnmul  15240  rei  15303  imi  15304  cji  15306  sqrtm1  15422  0.999...  16030  efival  16300  ef01bndlem  16332  5ndvds6  16564  3lcm2e6  16888  decsplit0b  17237  2exp8  17246  37prm  17279  43prm  17280  83prm  17281  139prm  17282  163prm  17283  317prm  17284  1259lem1  17289  1259lem2  17290  1259lem3  17291  1259lem4  17292  1259lem5  17293  2503lem1  17295  2503lem2  17296  2503prm  17298  4001lem1  17299  4001lem2  17300  4001lem3  17301  cnmsgnsubg  21863  mdetralt  22903  dveflem  26279  dvsincos  26281  efhalfpi  26782  pige3ALT  26830  cosne0  26839  efif1olem4  26855  logf1o2  26960  asin1  27204  dvatan  27245  log2ublem3  27258  log2ub  27259  birthday  27264  basellem9  27398  ppiub  27513  chtub  27521  bposlem8  27600  lgsdir2  27639  mulog2sumlem2  27844  pntlemb  27906  avril1  31046  ipidsq  31294  nmopadjlem  32673  nmopcoadji  32685  unierri  32688  signswch  35173  itgexpif  35218  reprlt  35231  breprexp  35245  hgt750lem  35263  hgt750lem2  35264  circum  36408  dvasin  38590  3lexlogpow5ineq1  43072  3lexlogpow5ineq5  43078  aks4d1p1  43094  235t711  43330  ex-decpmul  43331  it1ei  43341  sqrtcval2  44601  resqrtvalex  44604  imsqrtvalex  44605  inductionexd  45114  xralrple3  46329  wallispi  47024  wallispi2lem2  47026  stirlinglem1  47028  dirkertrigeqlem3  47054  goldpolyfactor  47871  goldratval  47880  modm1p1ne  48390  257prm  48590  fmtno4prmfac193  48602  fmtno5fac  48611  139prmALT  48625  127prm  48628  2exp340mod341  48775