Theorem mulridi 11248

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136  1c1 11139   · cmul 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-mulcl 11200  ax-mulcom 11202  ax-mulass 11204  ax-distr 11205  ax-1rid 11208  ax-cnre 11211

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423

This theorem is referenced by:  addrid  11424  0lt1  11766  muleqadd  11888  1t1e1  12404  2t1e2  12405  3t1e3  12407  halfpm6th  12463  9p1e10  12709  numltc  12733  numsucc  12747  dec10p  12750  numadd  12754  numaddc  12755  11multnc  12775  4t3lem  12804  5t2e10  12807  9t11e99  12837  nn0opthlem1  14259  faclbnd4lem1  14284  rei  15135  imi  15136  cji  15138  sqrtm1  15254  0.999...  15859  efival  16128  ef01bndlem  16160  3lcm2e6  16703  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  21508  mdetralt  22509  dveflem  25910  dvsincos  25912  efhalfpi  26405  pige3ALT  26453  cosne0  26462  efif1olem4  26478  logf1o2  26583  asin1  26825  dvatan  26866  log2ublem3  26879  log2ub  26880  birthday  26885  basellem9  27020  ppiub  27136  chtub  27144  bposlem8  27223  lgsdir2  27262  mulog2sumlem2  27467  pntlemb  27529  avril1  30272  ipidsq  30519  nmopadjlem  31898  nmopcoadji  31910  unierri  31913  sgnmul  34162  signswch  34193  itgexpif  34238  reprlt  34251  breprexp  34265  hgt750lem  34283  hgt750lem2  34284  circum  35278  dvasin  37177  3lexlogpow5ineq1  41525  3lexlogpow5ineq5  41531  aks4d1p1  41547  235t711  41867  ex-decpmul  41868  it1ei  41877  sqrtcval2  43072  resqrtvalex  43075  imsqrtvalex  43076  inductionexd  43585  xralrple3  44756  wallispi  45458  wallispi2lem2  45460  stirlinglem1  45462  dirkertrigeqlem3  45488  257prm  46901  fmtno4prmfac193  46913  fmtno5fac  46922  139prmALT  46936  127prm  46939  2exp340mod341  47073