Theorem mulridi 11123

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   · cmul 11018

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulcom 11077  ax-mulass 11079  ax-distr 11080  ax-1rid 11083  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  addrid  11300  0lt1  11646  muleqadd  11768  1t1e1  12289  2t1e2  12290  3t1e3  12292  9p1e10  12596  numltc  12620  numsucc  12634  dec10p  12637  numadd  12641  numaddc  12642  11multnc  12662  4t3lem  12691  5t2e10  12694  9t11e99  12724  nn0opthlem1  14177  faclbnd4lem1  14202  rei  15065  imi  15066  cji  15068  sqrtm1  15184  0.999...  15790  efival  16063  ef01bndlem  16095  5ndvds6  16327  3lcm2e6  16645  decsplit0b  16993  2exp8  17002  37prm  17034  43prm  17035  83prm  17036  139prm  17037  163prm  17038  317prm  17039  1259lem1  17044  1259lem2  17045  1259lem3  17046  1259lem4  17047  1259lem5  17048  2503lem1  17050  2503lem2  17051  2503prm  17053  4001lem1  17054  4001lem2  17055  4001lem3  17056  cnmsgnsubg  21516  mdetralt  22524  dveflem  25911  dvsincos  25913  efhalfpi  26408  pige3ALT  26457  cosne0  26466  efif1olem4  26482  logf1o2  26587  asin1  26832  dvatan  26873  log2ublem3  26886  log2ub  26887  birthday  26892  basellem9  27027  ppiub  27143  chtub  27151  bposlem8  27230  lgsdir2  27269  mulog2sumlem2  27474  pntlemb  27536  avril1  30445  ipidsq  30692  nmopadjlem  32071  nmopcoadji  32083  unierri  32086  sgnmul  32823  signswch  34595  itgexpif  34640  reprlt  34653  breprexp  34667  hgt750lem  34685  hgt750lem2  34686  circum  35739  dvasin  37764  3lexlogpow5ineq1  42167  3lexlogpow5ineq5  42173  aks4d1p1  42189  235t711  42423  ex-decpmul  42424  it1ei  42434  sqrtcval2  43759  resqrtvalex  43762  imsqrtvalex  43763  inductionexd  44272  xralrple3  45496  wallispi  46192  wallispi2lem2  46194  stirlinglem1  46196  dirkertrigeqlem3  46222  modm1p1ne  47494  257prm  47685  fmtno4prmfac193  47697  fmtno5fac  47706  139prmALT  47720  127prm  47723  2exp340mod341  47857