Theorem mulid2d 7188

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

Syntax hints:   -> wi 4   = wceq 1285   e. wcel 1434  (class class class)co 5537   CCcc 7030   1c1 7033   x. cmul 7037

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-resscn 7119  ax-1cn 7120  ax-icn 7122  ax-addcl 7123  ax-mulcl 7125  ax-mulcom 7128  ax-mulass 7130  ax-distr 7131  ax-1rid 7134  ax-cnre 7138

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3604  df-br 3788  df-iota 4891  df-fv 4934  df-ov 5540

This theorem is referenced by:  adddirp1d  7196  mulsubfacd  7578  mulcanapd  7807  receuap  7815  divdivdivap  7857  divcanap5  7858  ltrec  8017  recp1lt1  8033  nndivtr  8136  xp1d2m1eqxm1d2  8339  gtndiv  8512  lincmb01cmp  9090  iccf1o  9091  modqfrac  9408  qnegmod  9440  addmodid  9443  m1expcl2  9584  expgt1  9600  ltexp2a  9614  leexp2a  9615  binom3  9676  faclbnd  9754  facavg  9759  ibcval5  9776  cvg1nlemcau  9997  resqrexlemover  10023  resqrexlemcalc2  10028  absimle  10097  maxabslemlub  10220  iddvds  10342  gcdaddm  10508  rpmulgcd  10548  prmind2  10635  qdencn  10928