Theorem mullidd 8288

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 8268	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  1c1 8124   · cmul 8128

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8215  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-mulcom 8224  ax-mulass 8226  ax-distr 8227  ax-1rid 8230  ax-cnre 8234

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-iota 5311  df-fv 5359  df-ov 6052

This theorem is referenced by:  adddirp1d  8296  mulsubfacd  8688  mulcanapd  8931  receuap  8939  divdivdivap  8983  divcanap5  8984  subrecap  9109  ltrec  9153  recp1lt1  9169  nndivtr  9275  subhalfhalf  9469  xp1d2m1eqxm1d2  9487  gtndiv  9669  lincmb01cmp  10332  lincmble  10333  iccf1o  10334  modqfrac  10695  qnegmod  10727  addmodid  10730  m1expcl2  10919  expgt1  10935  ltexp2a  10949  leexp2a  10950  binom3  11015  faclbnd  11099  facavg  11104  bcval5  11121  cvg1nlemcau  11662  resqrexlemover  11688  resqrexlemcalc2  11693  absimle  11762  maxabslemlub  11885  reccn2ap  11991  binom1p  12164  binom1dif  12166  fprodsplitdc  12275  fprodcl2lem  12284  efcllemp  12337  ef01bndlem  12435  efieq1re  12451  eirraplem  12456  iddvds  12483  bitsfzolem  12633  bitsfzo  12634  gcdaddm  12673  rpmulgcd  12715  prmind2  12810  isprm5lem  12831  phiprm  12913  eulerthlemth  12922  fermltl  12924  hashgcdlem  12928  odzdvds  12936  powm2modprm  12943  modprm0  12945  pythagtriplem4  12959  4sqlem18  13099  mulgnnass  13863  dvexp  15563  dvef  15579  plypow  15596  reeff1oleme  15624  sin0pilem1  15633  sinhalfpip  15672  sinhalfpim  15673  coshalfpip  15674  coshalfpim  15675  tangtx  15690  logdivlti  15733  binom4  15831  pellexlem2  15833  wilthlem1  15835  mersenne  15852  perfectlem2  15855  lgsval2lem  15870  lgsval4a  15882  lgsneg1  15885  lgsdilem  15887  lgsdir2lem4  15891  lgsdir2  15893  lgsdir  15895  lgsmulsqcoprm  15906  lgsdirnn0  15907  lgsdinn0  15908  gausslemma2dlem1a  15918  gausslemma2dlem4  15924  gausslemma2dlem7  15928  gausslemma2d  15929  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem4  15933  lgsquad2lem1  15941  2sqlem8  15983  qdencn  16794