Theorem mulridi 11185

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   · cmul 11080

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  addrid  11361  0lt1  11707  muleqadd  11829  1t1e1  12350  2t1e2  12351  3t1e3  12353  9p1e10  12658  numltc  12682  numsucc  12696  dec10p  12699  numadd  12703  numaddc  12704  11multnc  12724  4t3lem  12753  5t2e10  12756  9t11e99  12786  nn0opthlem1  14240  faclbnd4lem1  14265  rei  15129  imi  15130  cji  15132  sqrtm1  15248  0.999...  15854  efival  16127  ef01bndlem  16159  5ndvds6  16391  3lcm2e6  16709  decsplit0b  17057  2exp8  17066  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  cnmsgnsubg  21493  mdetralt  22502  dveflem  25890  dvsincos  25892  efhalfpi  26387  pige3ALT  26436  cosne0  26445  efif1olem4  26461  logf1o2  26566  asin1  26811  dvatan  26852  log2ublem3  26865  log2ub  26866  birthday  26871  basellem9  27006  ppiub  27122  chtub  27130  bposlem8  27209  lgsdir2  27248  mulog2sumlem2  27453  pntlemb  27515  avril1  30399  ipidsq  30646  nmopadjlem  32025  nmopcoadji  32037  unierri  32040  sgnmul  32767  signswch  34559  itgexpif  34604  reprlt  34617  breprexp  34631  hgt750lem  34649  hgt750lem2  34650  circum  35668  dvasin  37705  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1  42071  235t711  42300  ex-decpmul  42301  it1ei  42311  sqrtcval2  43638  resqrtvalex  43641  imsqrtvalex  43642  inductionexd  44151  xralrple3  45377  wallispi  46075  wallispi2lem2  46077  stirlinglem1  46079  dirkertrigeqlem3  46105  modm1p1ne  47375  257prm  47566  fmtno4prmfac193  47578  fmtno5fac  47587  139prmALT  47601  127prm  47604  2exp340mod341  47738