Theorem mulridi 11178

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   · cmul 11073

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 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

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 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  addrid  11354  0lt1  11700  muleqadd  11822  1t1e1  12343  2t1e2  12344  3t1e3  12346  9p1e10  12651  numltc  12675  numsucc  12689  dec10p  12692  numadd  12696  numaddc  12697  11multnc  12717  4t3lem  12746  5t2e10  12749  9t11e99  12779  nn0opthlem1  14233  faclbnd4lem1  14258  rei  15122  imi  15123  cji  15125  sqrtm1  15241  0.999...  15847  efival  16120  ef01bndlem  16152  5ndvds6  16384  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  21486  mdetralt  22495  dveflem  25883  dvsincos  25885  efhalfpi  26380  pige3ALT  26429  cosne0  26438  efif1olem4  26454  logf1o2  26559  asin1  26804  dvatan  26845  log2ublem3  26858  log2ub  26859  birthday  26864  basellem9  26999  ppiub  27115  chtub  27123  bposlem8  27202  lgsdir2  27241  mulog2sumlem2  27446  pntlemb  27508  avril1  30392  ipidsq  30639  nmopadjlem  32018  nmopcoadji  32030  unierri  32033  sgnmul  32760  signswch  34552  itgexpif  34597  reprlt  34610  breprexp  34624  hgt750lem  34642  hgt750lem2  34643  circum  35661  dvasin  37698  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  235t711  42293  ex-decpmul  42294  it1ei  42304  sqrtcval2  43631  resqrtvalex  43634  imsqrtvalex  43635  inductionexd  44144  xralrple3  45370  wallispi  46068  wallispi2lem2  46070  stirlinglem1  46072  dirkertrigeqlem3  46098  modm1p1ne  47371  257prm  47562  fmtno4prmfac193  47574  fmtno5fac  47583  139prmALT  47597  127prm  47600  2exp340mod341  47734