Theorem mullidd 8344

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  1c1 8180   · cmul 8184

This proof depends on 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 8271  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-mulcom 8280  ax-mulass 8282  ax-distr 8283  ax-1rid 8286  ax-cnre 8290

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  adddirp1d  8352  mulsubfacd  8746  mulcanapd  8990  receuap  9000  divdivdivap  9044  divcanap5  9045  subrecap  9170  ltrec  9214  recp1lt1  9230  nndivtr  9347  subhalfhalf  9542  xp1d2m1eqxm1d2  9560  gtndiv  9743  lincmb01cmp  10407  lincmble  10408  iccf1o  10409  modqfrac  10776  qnegmod  10808  addmodid  10811  m1expcl2  11000  expgt1  11016  ltexp2a  11030  leexp2a  11031  binom3  11096  faclbnd  11181  facavg  11186  bcval5  11203  sq01  11662  cvg1nlemcau  11752  resqrexlemover  11778  resqrexlemcalc2  11783  absimle  11852  maxabslemlub  11975  reccn2ap  12081  binom1p  12254  binom1dif  12256  fprodsplitdc  12365  fprodcl2lem  12374  efcllemp  12427  ef01bndlem  12525  efieq1re  12541  eirraplem  12546  iddvds  12573  bitsfzolem  12723  bitsfzo  12724  gcdaddm  12763  rpmulgcd  12805  prmind2  12900  isprm5lem  12921  phiprm  13003  eulerthlemth  13012  fermltl  13014  hashgcdlem  13018  odzdvds  13026  powm2modprm  13033  modprm0  13035  pythagtriplem4  13049  4sqlem18  13189  mulgnnass  13962  dvexp  15814  dvef  15830  plypow  15847  reeff1oleme  15875  sin0pilem1  15885  sinhalfpip  15924  sinhalfpim  15925  coshalfpip  15926  coshalfpim  15927  tangtx  15942  logdivlti  15986  logfac  16001  binom4  16087  pellexlem2  16098  wilthlem1  16100  mersenne  16117  perfectlem2  16120  lgsval2lem  16141  lgsval4a  16153  lgsneg1  16156  lgsdilem  16158  lgsdir2lem4  16162  lgsdir2  16164  lgsdir  16166  lgsmulsqcoprm  16177  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem4  16195  gausslemma2dlem7  16199  gausslemma2d  16200  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem4  16204  lgsquad2lem1  16212  2sqlem8  16254  qdencn  17084