Theorem mulid2d 7913

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136  (class class class)co 5841   CCcc 7747   1c1 7750   x. cmul 7754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841  ax-1cn 7842  ax-icn 7844  ax-addcl 7845  ax-mulcl 7847  ax-mulcom 7850  ax-mulass 7852  ax-distr 7853  ax-1rid 7856  ax-cnre 7860

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  adddirp1d  7921  mulsubfacd  8312  mulcanapd  8554  receuap  8562  divdivdivap  8605  divcanap5  8606  subrecap  8731  ltrec  8774  recp1lt1  8790  nndivtr  8895  xp1d2m1eqxm1d2  9105  gtndiv  9282  lincmb01cmp  9935  iccf1o  9936  modqfrac  10268  qnegmod  10300  addmodid  10303  m1expcl2  10473  expgt1  10489  ltexp2a  10503  leexp2a  10504  binom3  10568  faclbnd  10650  facavg  10655  bcval5  10672  cvg1nlemcau  10922  resqrexlemover  10948  resqrexlemcalc2  10953  absimle  11022  maxabslemlub  11145  reccn2ap  11250  binom1p  11422  binom1dif  11424  fprodsplitdc  11533  fprodcl2lem  11542  efcllemp  11595  ef01bndlem  11693  efieq1re  11708  eirraplem  11713  iddvds  11740  gcdaddm  11913  rpmulgcd  11955  prmind2  12048  isprm5lem  12069  phiprm  12151  eulerthlemth  12160  fermltl  12162  hashgcdlem  12166  odzdvds  12173  powm2modprm  12180  modprm0  12182  pythagtriplem4  12196  dvexp  13275  dvef  13288  reeff1oleme  13293  sin0pilem1  13302  sinhalfpip  13341  sinhalfpim  13342  coshalfpip  13343  coshalfpim  13344  tangtx  13359  logdivlti  13402  binom4  13497  lgsval2lem  13511  lgsval4a  13523  lgsneg1  13526  lgsdilem  13528  lgsdir2lem4  13532  lgsdir2  13534  lgsdir  13536  lgsmulsqcoprm  13547  lgsdirnn0  13548  lgsdinn0  13549  2sqlem8  13559  qdencn  13866