Theorem mulid1i 10042

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

Syntax hints:   = wceq 1483   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934  1c1 9937   · cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  addid1  10216  0lt1  10550  muleqadd  10671  1t1e1  11175  2t1e2  11176  3t1e3  11178  halfpm6th  11253  9p1e10  11496  numltc  11528  numsucc  11549  dec10p  11553  dec10pOLD  11554  numadd  11560  numaddc  11561  11multnc  11592  4t3lem  11631  5t2e10  11634  9t11e99  11671  9t11e99OLD  11672  nn0opthlem1  13055  faclbnd4lem1  13080  rei  13896  imi  13897  cji  13899  sqrtm1  14016  0.999...  14612  0.999...OLD  14613  efival  14882  ef01bndlem  14914  3lcm2e6  15440  decsplit0b  15784  decsplit0bOLD  15788  2exp8  15796  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  cnmsgnsubg  19923  mdetralt  20414  dveflem  23742  dvsincos  23744  efhalfpi  24223  pige3  24269  cosne0  24276  efif1olem4  24291  logf1o2  24396  asin1  24621  dvatan  24662  log2ublem3  24675  log2ub  24676  birthday  24681  basellem9  24815  ppiub  24929  chtub  24937  bposlem8  25016  lgsdir2  25055  mulog2sumlem2  25224  pntlemb  25286  avril1  27319  ipidsq  27565  nmopadjlem  28948  nmopcoadji  28960  unierri  28963  sgnmul  30604  signswch  30638  itgexpif  30684  reprlt  30697  breprexp  30711  hgt750lem  30729  hgt750lem2  30730  circum  31568  dvasin  33496  inductionexd  38453  xralrple3  39590  wallispi  40287  wallispi2lem2  40289  stirlinglem1  40291  dirkertrigeqlem3  40317  257prm  41473  fmtno4prmfac193  41485  fmtno5fac  41494  139prmALT  41511  127prm  41515