Theorem mulid1d 7559

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulid1d	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulid1d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid1 7539	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1290   ∈ wcel 1439  (class class class)co 5666  ℂcc 7402  1c1 7405   · cmul 7409

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-resscn 7491  ax-1cn 7492  ax-icn 7494  ax-addcl 7495  ax-mulcl 7497  ax-mulcom 7500  ax-mulass 7502  ax-distr 7503  ax-1rid 7506  ax-cnre 7510

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669

This theorem is referenced by:  muladd11  7669  ltmul1  8123  mulap0  8177  divrecap  8209  diveqap1  8226  conjmulap  8250  apmul1  8309  qapne  9178  divelunit  9473  modqid  9810  q2submod  9846  addmodlteq  9859  expadd  10051  leexp2r  10063  nnlesq  10112  sqoddm1div8  10160  nn0opthlem1d  10182  faclbnd  10203  faclbnd2  10204  faclbnd6  10206  facavg  10208  bcn0  10217  bcn1  10220  hash2iun1dif1  10928  binom11  10934  trireciplem  10948  geosergap  10954  cvgratnnlemnexp  10972  cvgratnnlemmn  10973  efzval  11027  tanaddaplem  11083  tanaddap  11084  cos01gt0  11107  absef  11113  1dvds  11142  bezoutlema  11320  bezoutlemb  11321  gcdmultiple  11341  sqgcd  11350  lcm1  11395  coprmdvds  11406  qredeu  11411  phiprmpw  11530