Theorem mulid2d 8121

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

Hypothesis

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

Assertion

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

Proof of Theorem mulid2d

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5962  ℂcc 7953  1c1 7956   · cmul 7960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8047  ax-1cn 8048  ax-icn 8050  ax-addcl 8051  ax-mulcl 8053  ax-mulcom 8056  ax-mulass 8058  ax-distr 8059  ax-1rid 8062  ax-cnre 8066

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-iota 5246  df-fv 5293  df-ov 5965

This theorem is referenced by:  adddirp1d  8129  mulsubfacd  8521  mulcanapd  8764  receuap  8772  divdivdivap  8816  divcanap5  8817  subrecap  8942  ltrec  8986  recp1lt1  9002  nndivtr  9108  xp1d2m1eqxm1d2  9320  gtndiv  9498  lincmb01cmp  10155  iccf1o  10156  modqfrac  10514  qnegmod  10546  addmodid  10549  m1expcl2  10738  expgt1  10754  ltexp2a  10768  leexp2a  10769  binom3  10834  faclbnd  10918  facavg  10923  bcval5  10940  cvg1nlemcau  11380  resqrexlemover  11406  resqrexlemcalc2  11411  absimle  11480  maxabslemlub  11603  reccn2ap  11709  binom1p  11881  binom1dif  11883  fprodsplitdc  11992  fprodcl2lem  12001  efcllemp  12054  ef01bndlem  12152  efieq1re  12168  eirraplem  12173  iddvds  12200  gcdaddm  12390  rpmulgcd  12432  prmind2  12527  isprm5lem  12548  phiprm  12630  eulerthlemth  12639  fermltl  12641  hashgcdlem  12645  odzdvds  12653  powm2modprm  12660  modprm0  12662  pythagtriplem4  12676  mulgnnass  13578  dvexp  15268  dvef  15284  reeff1oleme  15329  sin0pilem1  15338  sinhalfpip  15377  sinhalfpim  15378  coshalfpip  15379  coshalfpim  15380  tangtx  15395  logdivlti  15438  binom4  15536  lgsval2lem  15572  lgsval4a  15584  lgsneg1  15587  lgsdilem  15589  lgsdir2lem4  15593  lgsdir2  15595  lgsdir  15597  lgsmulsqcoprm  15608  lgsdirnn0  15609  lgsdinn0  15610  2sqlem8  15685  qdencn  16138