Theorem mulid2d 7975

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 7954	. 2 |- ( A e. CC -> ( 1 x. A ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( 1 x. A ) = A )

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5874   CCcc 7808   1c1 7811   x. cmul 7815

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1cn 7903  ax-icn 7905  ax-addcl 7906  ax-mulcl 7908  ax-mulcom 7911  ax-mulass 7913  ax-distr 7914  ax-1rid 7917  ax-cnre 7921

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  adddirp1d  7983  mulsubfacd  8374  mulcanapd  8617  receuap  8625  divdivdivap  8669  divcanap5  8670  subrecap  8795  ltrec  8839  recp1lt1  8855  nndivtr  8960  xp1d2m1eqxm1d2  9170  gtndiv  9347  lincmb01cmp  10002  iccf1o  10003  modqfrac  10336  qnegmod  10368  addmodid  10371  m1expcl2  10541  expgt1  10557  ltexp2a  10571  leexp2a  10572  binom3  10637  faclbnd  10720  facavg  10725  bcval5  10742  cvg1nlemcau  10992  resqrexlemover  11018  resqrexlemcalc2  11023  absimle  11092  maxabslemlub  11215  reccn2ap  11320  binom1p  11492  binom1dif  11494  fprodsplitdc  11603  fprodcl2lem  11612  efcllemp  11665  ef01bndlem  11763  efieq1re  11778  eirraplem  11783  iddvds  11810  gcdaddm  11984  rpmulgcd  12026  prmind2  12119  isprm5lem  12140  phiprm  12222  eulerthlemth  12231  fermltl  12233  hashgcdlem  12237  odzdvds  12244  powm2modprm  12251  modprm0  12253  pythagtriplem4  12267  mulgnnass  13016  dvexp  14145  dvef  14158  reeff1oleme  14163  sin0pilem1  14172  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  tangtx  14229  logdivlti  14272  binom4  14367  lgsval2lem  14381  lgsval4a  14393  lgsneg1  14396  lgsdilem  14398  lgsdir2lem4  14402  lgsdir2  14404  lgsdir  14406  lgsmulsqcoprm  14417  lgsdirnn0  14418  lgsdinn0  14419  2sqlem8  14440  qdencn  14745