Theorem mulridi 11149

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 7367  ℂ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 2708  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 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  addrid  11326  0lt1  11672  muleqadd  11794  1t1e1  12338  2t1e2  12339  3t1e3  12341  9p1e10  12646  numltc  12670  numsucc  12684  dec10p  12687  numadd  12691  numaddc  12692  11multnc  12712  4t3lem  12741  5t2e10  12744  9t11e99  12774  nn0opthlem1  14230  faclbnd4lem1  14255  rei  15118  imi  15119  cji  15121  sqrtm1  15237  0.999...  15846  efival  16119  ef01bndlem  16151  5ndvds6  16383  3lcm2e6  16702  decsplit0b  17050  2exp8  17059  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  cnmsgnsubg  21557  mdetralt  22573  dveflem  25946  dvsincos  25948  efhalfpi  26435  pige3ALT  26484  cosne0  26493  efif1olem4  26509  logf1o2  26614  asin1  26858  dvatan  26899  log2ublem3  26912  log2ub  26913  birthday  26918  basellem9  27052  ppiub  27167  chtub  27175  bposlem8  27254  lgsdir2  27293  mulog2sumlem2  27498  pntlemb  27560  avril1  30533  ipidsq  30781  nmopadjlem  32160  nmopcoadji  32172  unierri  32175  sgnmul  32908  signswch  34705  itgexpif  34750  reprlt  34763  breprexp  34777  hgt750lem  34795  hgt750lem2  34796  circum  35856  dvasin  38025  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1  42515  235t711  42737  ex-decpmul  42738  it1ei  42748  sqrtcval2  44069  resqrtvalex  44072  imsqrtvalex  44073  inductionexd  44582  xralrple3  45803  wallispi  46498  wallispi2lem2  46500  stirlinglem1  46502  dirkertrigeqlem3  46528  modm1p1ne  47824  257prm  48024  fmtno4prmfac193  48036  fmtno5fac  48045  139prmALT  48059  127prm  48062  2exp340mod341  48209