Theorem mullidd 8350

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

Hypothesis

Ref	Expression
addcld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mullidd	|- ( ph -> ( 1 x. A ) = A )

Proof of Theorem mullidd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		mullid 8330	. 2 |- ( A e. CC -> ( 1 x. A ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( 1 x. A ) = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   1c1 8186   x. cmul 8190

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 8277  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-mulcom 8286  ax-mulass 8288  ax-distr 8289  ax-1rid 8292  ax-cnre 8296

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  adddirp1d  8358  mulsubfacd  8753  mulcanapd  8997  receuap  9007  divdivdivap  9051  divcanap5  9052  subrecap  9177  ltrec  9221  recp1lt1  9237  nndivtr  9355  subhalfhalf  9551  xp1d2m1eqxm1d2  9569  gtndiv  9751  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  modqfrac  10794  qnegmod  10826  addmodid  10829  m1expcl2  11018  expgt1  11034  ltexp2a  11048  leexp2a  11049  binom3  11114  faclbnd  11200  facavg  11205  bcval5  11222  sq01  11681  cvg1nlemcau  11771  resqrexlemover  11797  resqrexlemcalc2  11802  absimle  11872  maxabslemlub  11995  reccn2ap  12103  binom1p  12276  binom1dif  12278  fprodsplitdc  12387  fprodcl2lem  12396  efcllemp  12449  ef01bndlem  12547  efieq1re  12563  eirraplem  12568  iddvds  12595  bitsfzolem  12745  bitsfzo  12746  gcdaddm  12785  rpmulgcd  12827  prmind2  12922  isprm5lem  12944  phiprm  13029  eulerthlemth  13038  fermltl  13040  hashgcdlem  13044  odzdvds  13052  powm2modprm  13059  modprm0  13061  pythagtriplem4  13075  4sqlem18  13215  mulgnnass  14018  dvexp  15954  dvef  15970  plypow  15987  reeff1oleme  16015  sin0pilem1  16025  sinhalfpip  16064  sinhalfpim  16065  coshalfpip  16066  coshalfpim  16067  tangtx  16082  logdivlti  16128  logfac  16143  binom4  16236  pellexlem2  16247  wilthlem1  16249  mersenne  16314  perfectlem2  16317  bposlem2  16329  bposlem9  16336  lgsval2lem  16351  lgsval4a  16363  lgsneg1  16366  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2  16374  lgsdir  16376  lgsmulsqcoprm  16387  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem4  16414  lgsquad2lem1  16422  2sqlem8  16464  qdencn  17295