Theorem mulid1i 10979

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulid1i	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulid1i

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulid1 10973	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  1c1 10872   · cmul 10876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-mulcom 10935  ax-mulass 10937  ax-distr 10938  ax-1rid 10941  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  addid1  11155  0lt1  11497  muleqadd  11619  1t1e1  12135  2t1e2  12136  3t1e3  12138  halfpm6th  12194  9p1e10  12439  numltc  12463  numsucc  12477  dec10p  12480  numadd  12484  numaddc  12485  11multnc  12505  4t3lem  12534  5t2e10  12537  9t11e99  12567  nn0opthlem1  13982  faclbnd4lem1  14007  rei  14867  imi  14868  cji  14870  sqrtm1  14987  0.999...  15593  efival  15861  ef01bndlem  15893  3lcm2e6  16436  decsplit0b  16781  2exp8  16790  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  1259lem1  16832  1259lem2  16833  1259lem3  16834  1259lem4  16835  1259lem5  16836  2503lem1  16838  2503lem2  16839  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem3  16844  cnmsgnsubg  20782  mdetralt  21757  dveflem  25143  dvsincos  25145  efhalfpi  25628  pige3ALT  25676  cosne0  25685  efif1olem4  25701  logf1o2  25805  asin1  26044  dvatan  26085  log2ublem3  26098  log2ub  26099  birthday  26104  basellem9  26238  ppiub  26352  chtub  26360  bposlem8  26439  lgsdir2  26478  mulog2sumlem2  26683  pntlemb  26745  avril1  28827  ipidsq  29072  nmopadjlem  30451  nmopcoadji  30463  unierri  30466  sgnmul  32509  signswch  32540  itgexpif  32586  reprlt  32599  breprexp  32613  hgt750lem  32631  hgt750lem2  32632  circum  33632  dvasin  35861  3lexlogpow5ineq1  40062  3lexlogpow5ineq5  40068  aks4d1p1  40084  235t711  40319  ex-decpmul  40320  sqrtcval2  41250  resqrtvalex  41253  imsqrtvalex  41254  inductionexd  41765  xralrple3  42913  wallispi  43611  wallispi2lem2  43613  stirlinglem1  43615  dirkertrigeqlem3  43641  257prm  45013  fmtno4prmfac193  45025  fmtno5fac  45034  139prmALT  45048  127prm  45051  2exp340mod341  45185