Theorem mulid2d 8024

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

Hypothesis

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

Assertion

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

Proof of Theorem mulid2d

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160  (class class class)co 5906   CCcc 7856   1c1 7859   x. cmul 7863

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7950  ax-1cn 7951  ax-icn 7953  ax-addcl 7954  ax-mulcl 7956  ax-mulcom 7959  ax-mulass 7961  ax-distr 7962  ax-1rid 7965  ax-cnre 7969

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2758  df-un 3153  df-in 3155  df-ss 3162  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-br 4026  df-iota 5203  df-fv 5250  df-ov 5909

This theorem is referenced by:  adddirp1d  8032  mulsubfacd  8423  mulcanapd  8666  receuap  8674  divdivdivap  8718  divcanap5  8719  subrecap  8844  ltrec  8888  recp1lt1  8904  nndivtr  9010  xp1d2m1eqxm1d2  9221  gtndiv  9398  lincmb01cmp  10055  iccf1o  10056  modqfrac  10394  qnegmod  10426  addmodid  10429  m1expcl2  10606  expgt1  10622  ltexp2a  10636  leexp2a  10637  binom3  10702  faclbnd  10786  facavg  10791  bcval5  10808  cvg1nlemcau  11102  resqrexlemover  11128  resqrexlemcalc2  11133  absimle  11202  maxabslemlub  11325  reccn2ap  11430  binom1p  11602  binom1dif  11604  fprodsplitdc  11713  fprodcl2lem  11722  efcllemp  11775  ef01bndlem  11873  efieq1re  11889  eirraplem  11894  iddvds  11921  gcdaddm  12095  rpmulgcd  12137  prmind2  12232  isprm5lem  12253  phiprm  12335  eulerthlemth  12344  fermltl  12346  hashgcdlem  12350  odzdvds  12357  powm2modprm  12364  modprm0  12366  pythagtriplem4  12380  mulgnnass  13201  dvexp  14817  dvef  14830  reeff1oleme  14835  sin0pilem1  14844  sinhalfpip  14883  sinhalfpim  14884  coshalfpip  14885  coshalfpim  14886  tangtx  14901  logdivlti  14944  binom4  15039  lgsval2lem  15054  lgsval4a  15066  lgsneg1  15069  lgsdilem  15071  lgsdir2lem4  15075  lgsdir2  15077  lgsdir  15079  lgsmulsqcoprm  15090  lgsdirnn0  15091  lgsdinn0  15092  2sqlem8  15134  qdencn  15441