Theorem mullidd 8345

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 8325	. 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 6085   CCcc 8178   1c1 8181   x. cmul 8185

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 8272  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-mulcom 8281  ax-mulass 8283  ax-distr 8284  ax-1rid 8287  ax-cnre 8291

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  8353  mulsubfacd  8748  mulcanapd  8992  receuap  9002  divdivdivap  9046  divcanap5  9047  subrecap  9172  ltrec  9216  recp1lt1  9232  nndivtr  9349  subhalfhalf  9545  xp1d2m1eqxm1d2  9563  gtndiv  9746  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  modqfrac  10789  qnegmod  10821  addmodid  10824  m1expcl2  11013  expgt1  11029  ltexp2a  11043  leexp2a  11044  binom3  11109  faclbnd  11195  facavg  11200  bcval5  11217  sq01  11676  cvg1nlemcau  11766  resqrexlemover  11792  resqrexlemcalc2  11797  absimle  11867  maxabslemlub  11990  reccn2ap  12098  binom1p  12271  binom1dif  12273  fprodsplitdc  12382  fprodcl2lem  12391  efcllemp  12444  ef01bndlem  12542  efieq1re  12558  eirraplem  12563  iddvds  12590  bitsfzolem  12740  bitsfzo  12741  gcdaddm  12780  rpmulgcd  12822  prmind2  12917  isprm5lem  12939  phiprm  13024  eulerthlemth  13033  fermltl  13035  hashgcdlem  13039  odzdvds  13047  powm2modprm  13054  modprm0  13056  pythagtriplem4  13070  4sqlem18  13210  mulgnnass  14013  dvexp  15903  dvef  15919  plypow  15936  reeff1oleme  15964  sin0pilem1  15974  sinhalfpip  16013  sinhalfpim  16014  coshalfpip  16015  coshalfpim  16016  tangtx  16031  logdivlti  16075  logfac  16090  binom4  16180  pellexlem2  16191  wilthlem1  16193  mersenne  16258  perfectlem2  16261  bposlem2  16273  bposlem9  16280  lgsval2lem  16295  lgsval4a  16307  lgsneg1  16310  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2  16318  lgsdir  16320  lgsmulsqcoprm  16331  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem4  16358  lgsquad2lem1  16366  2sqlem8  16408  qdencn  17238