Theorem mullidd 8338

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

Hypothesis

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

Assertion

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

Proof of Theorem mullidd

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171  1c1 8174   · cmul 8178

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8265  ax-1cn 8266  ax-icn 8268  ax-addcl 8269  ax-mulcl 8271  ax-mulcom 8274  ax-mulass 8276  ax-distr 8277  ax-1rid 8280  ax-cnre 8284

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082

This theorem is referenced by:  adddirp1d  8346  mulsubfacd  8740  mulcanapd  8983  receuap  8993  divdivdivap  9037  divcanap5  9038  subrecap  9163  ltrec  9207  recp1lt1  9223  nndivtr  9329  subhalfhalf  9523  xp1d2m1eqxm1d2  9541  gtndiv  9724  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  modqfrac  10757  qnegmod  10789  addmodid  10792  m1expcl2  10981  expgt1  10997  ltexp2a  11011  leexp2a  11012  binom3  11077  faclbnd  11162  facavg  11167  bcval5  11184  sq01  11643  cvg1nlemcau  11733  resqrexlemover  11759  resqrexlemcalc2  11764  absimle  11833  maxabslemlub  11956  reccn2ap  12062  binom1p  12235  binom1dif  12237  fprodsplitdc  12346  fprodcl2lem  12355  efcllemp  12408  ef01bndlem  12506  efieq1re  12522  eirraplem  12527  iddvds  12554  bitsfzolem  12704  bitsfzo  12705  gcdaddm  12744  rpmulgcd  12786  prmind2  12881  isprm5lem  12902  phiprm  12984  eulerthlemth  12993  fermltl  12995  hashgcdlem  12999  odzdvds  13007  powm2modprm  13014  modprm0  13016  pythagtriplem4  13030  4sqlem18  13170  mulgnnass  13943  dvexp  15795  dvef  15811  plypow  15828  reeff1oleme  15856  sin0pilem1  15865  sinhalfpip  15904  sinhalfpim  15905  coshalfpip  15906  coshalfpim  15907  tangtx  15922  logdivlti  15965  logfac  15978  binom4  16064  pellexlem2  16075  wilthlem1  16077  mersenne  16094  perfectlem2  16097  lgsval2lem  16112  lgsval4a  16124  lgsneg1  16127  lgsdilem  16129  lgsdir2lem4  16133  lgsdir2  16135  lgsdir  16137  lgsmulsqcoprm  16148  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem4  16166  gausslemma2dlem7  16170  gausslemma2d  16171  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem4  16175  lgsquad2lem1  16183  2sqlem8  16225  qdencn  17046