Theorem mulridi 11147

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulcom 11100  ax-mulass 11102  ax-distr 11103  ax-1rid 11106  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  addrid  11324  0lt1  11670  muleqadd  11792  1t1e1  12336  2t1e2  12337  3t1e3  12339  9p1e10  12644  numltc  12668  numsucc  12682  dec10p  12685  numadd  12689  numaddc  12690  11multnc  12710  4t3lem  12739  5t2e10  12742  9t11e99  12772  nn0opthlem1  14228  faclbnd4lem1  14253  rei  15116  imi  15117  cji  15119  sqrtm1  15235  0.999...  15844  efival  16117  ef01bndlem  16149  5ndvds6  16381  3lcm2e6  16700  decsplit0b  17048  2exp8  17057  37prm  17089  43prm  17090  83prm  17091  139prm  17092  163prm  17093  317prm  17094  1259lem1  17099  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  2503lem1  17105  2503lem2  17106  2503prm  17108  4001lem1  17109  4001lem2  17110  4001lem3  17111  cnmsgnsubg  21559  mdetralt  22598  dveflem  25971  dvsincos  25973  efhalfpi  26460  pige3ALT  26509  cosne0  26518  efif1olem4  26534  logf1o2  26639  asin1  26883  dvatan  26924  log2ublem3  26937  log2ub  26938  birthday  26943  basellem9  27077  ppiub  27192  chtub  27200  bposlem8  27279  lgsdir2  27318  mulog2sumlem2  27523  pntlemb  27585  avril1  30558  ipidsq  30806  nmopadjlem  32185  nmopcoadji  32197  unierri  32200  sgnmul  32934  signswch  34752  itgexpif  34797  reprlt  34810  breprexp  34824  hgt750lem  34842  hgt750lem2  34843  circum  35909  dvasin  38078  3lexlogpow5ineq1  42546  3lexlogpow5ineq5  42552  aks4d1p1  42568  235t711  42789  ex-decpmul  42790  it1ei  42800  sqrtcval2  44093  resqrtvalex  44096  imsqrtvalex  44097  inductionexd  44606  xralrple3  45825  wallispi  46520  wallispi2lem2  46522  stirlinglem1  46524  dirkertrigeqlem3  46550  modm1p1ne  47846  257prm  48046  fmtno4prmfac193  48058  fmtno5fac  48067  139prmALT  48081  127prm  48084  2exp340mod341  48231