Theorem mulid2d 8011

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 7990	. 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 5900   CCcc 7844   1c1 7847   x. cmul 7851

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 7938  ax-1cn 7939  ax-icn 7941  ax-addcl 7942  ax-mulcl 7944  ax-mulcom 7947  ax-mulass 7949  ax-distr 7950  ax-1rid 7953  ax-cnre 7957

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 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-br 4022  df-iota 5199  df-fv 5246  df-ov 5903

This theorem is referenced by:  adddirp1d  8019  mulsubfacd  8410  mulcanapd  8653  receuap  8661  divdivdivap  8705  divcanap5  8706  subrecap  8831  ltrec  8875  recp1lt1  8891  nndivtr  8996  xp1d2m1eqxm1d2  9206  gtndiv  9383  lincmb01cmp  10039  iccf1o  10040  modqfrac  10374  qnegmod  10406  addmodid  10409  m1expcl2  10582  expgt1  10598  ltexp2a  10612  leexp2a  10613  binom3  10678  faclbnd  10762  facavg  10767  bcval5  10784  cvg1nlemcau  11034  resqrexlemover  11060  resqrexlemcalc2  11065  absimle  11134  maxabslemlub  11257  reccn2ap  11362  binom1p  11534  binom1dif  11536  fprodsplitdc  11645  fprodcl2lem  11654  efcllemp  11707  ef01bndlem  11805  efieq1re  11820  eirraplem  11825  iddvds  11852  gcdaddm  12026  rpmulgcd  12068  prmind2  12163  isprm5lem  12184  phiprm  12266  eulerthlemth  12275  fermltl  12277  hashgcdlem  12281  odzdvds  12288  powm2modprm  12295  modprm0  12297  pythagtriplem4  12311  mulgnnass  13122  dvexp  14660  dvef  14673  reeff1oleme  14678  sin0pilem1  14687  sinhalfpip  14726  sinhalfpim  14727  coshalfpip  14728  coshalfpim  14729  tangtx  14744  logdivlti  14787  binom4  14882  lgsval2lem  14897  lgsval4a  14909  lgsneg1  14912  lgsdilem  14914  lgsdir2lem4  14918  lgsdir2  14920  lgsdir  14922  lgsmulsqcoprm  14933  lgsdirnn0  14934  lgsdinn0  14935  2sqlem8  14956  qdencn  15263