Theorem mulridi 11217

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7402  ℂcc 11105  1c1 11108   · cmul 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-mulcom 11171  ax-mulass 11173  ax-distr 11174  ax-1rid 11177  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405

This theorem is referenced by:  addrid  11393  0lt1  11735  muleqadd  11857  1t1e1  12373  2t1e2  12374  3t1e3  12376  halfpm6th  12432  9p1e10  12678  numltc  12702  numsucc  12716  dec10p  12719  numadd  12723  numaddc  12724  11multnc  12744  4t3lem  12773  5t2e10  12776  9t11e99  12806  nn0opthlem1  14229  faclbnd4lem1  14254  rei  15105  imi  15106  cji  15108  sqrtm1  15224  0.999...  15829  efival  16098  ef01bndlem  16130  3lcm2e6  16673  decsplit0b  17018  2exp8  17027  37prm  17059  43prm  17060  83prm  17061  139prm  17062  163prm  17063  317prm  17064  1259lem1  17069  1259lem2  17070  1259lem3  17071  1259lem4  17072  1259lem5  17073  2503lem1  17075  2503lem2  17076  2503prm  17078  4001lem1  17079  4001lem2  17080  4001lem3  17081  cnmsgnsubg  21459  mdetralt  22454  dveflem  25855  dvsincos  25857  efhalfpi  26346  pige3ALT  26394  cosne0  26403  efif1olem4  26419  logf1o2  26524  asin1  26766  dvatan  26807  log2ublem3  26820  log2ub  26821  birthday  26826  basellem9  26961  ppiub  27077  chtub  27085  bposlem8  27164  lgsdir2  27203  mulog2sumlem2  27408  pntlemb  27470  avril1  30210  ipidsq  30457  nmopadjlem  31836  nmopcoadji  31848  unierri  31851  sgnmul  34060  signswch  34091  itgexpif  34136  reprlt  34149  breprexp  34163  hgt750lem  34181  hgt750lem2  34182  circum  35176  dvasin  37075  3lexlogpow5ineq1  41425  3lexlogpow5ineq5  41431  aks4d1p1  41447  235t711  41735  ex-decpmul  41736  it1ei  41745  sqrtcval2  42942  resqrtvalex  42945  imsqrtvalex  42946  inductionexd  43455  xralrple3  44629  wallispi  45331  wallispi2lem2  45333  stirlinglem1  45335  dirkertrigeqlem3  45361  257prm  46774  fmtno4prmfac193  46786  fmtno5fac  46795  139prmALT  46809  127prm  46812  2exp340mod341  46946