Theorem mulid2d 8197

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   1c1 8032   x. cmul 8036

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-mulcom 8132  ax-mulass 8134  ax-distr 8135  ax-1rid 8138  ax-cnre 8142

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  adddirp1d  8205  mulsubfacd  8597  mulcanapd  8840  receuap  8848  divdivdivap  8892  divcanap5  8893  subrecap  9018  ltrec  9062  recp1lt1  9078  nndivtr  9184  xp1d2m1eqxm1d2  9396  gtndiv  9574  lincmb01cmp  10237  iccf1o  10238  modqfrac  10598  qnegmod  10630  addmodid  10633  m1expcl2  10822  expgt1  10838  ltexp2a  10852  leexp2a  10853  binom3  10918  faclbnd  11002  facavg  11007  bcval5  11024  cvg1nlemcau  11544  resqrexlemover  11570  resqrexlemcalc2  11575  absimle  11644  maxabslemlub  11767  reccn2ap  11873  binom1p  12045  binom1dif  12047  fprodsplitdc  12156  fprodcl2lem  12165  efcllemp  12218  ef01bndlem  12316  efieq1re  12332  eirraplem  12337  iddvds  12364  gcdaddm  12554  rpmulgcd  12596  prmind2  12691  isprm5lem  12712  phiprm  12794  eulerthlemth  12803  fermltl  12805  hashgcdlem  12809  odzdvds  12817  powm2modprm  12824  modprm0  12826  pythagtriplem4  12840  mulgnnass  13743  dvexp  15434  dvef  15450  reeff1oleme  15495  sin0pilem1  15504  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  tangtx  15561  logdivlti  15604  binom4  15702  lgsval2lem  15738  lgsval4a  15750  lgsneg1  15753  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2  15761  lgsdir  15763  lgsmulsqcoprm  15774  lgsdirnn0  15775  lgsdinn0  15776  2sqlem8  15851  qdencn  16631