Theorem mulid1d 7408

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mulid1d	|- ( ph -> ( A x. 1 ) = A )

Proof of Theorem mulid1d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		mulid1 7388	. 2 |- ( A e. CC -> ( A x. 1 ) = A )
3	1, 2	syl 14	1 |- ( ph -> ( A x. 1 ) = A )

Syntax hints:   -> wi 4   = wceq 1285   e. wcel 1434  (class class class)co 5591   CCcc 7251   1c1 7254   x. cmul 7258

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 2065  ax-resscn 7340  ax-1cn 7341  ax-icn 7343  ax-addcl 7344  ax-mulcl 7346  ax-mulcom 7349  ax-mulass 7351  ax-distr 7352  ax-1rid 7355  ax-cnre 7359

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-iota 4934  df-fv 4977  df-ov 5594

This theorem is referenced by:  muladd11  7518  ltmul1  7969  mulap0  8021  divrecap  8053  diveqap1  8070  conjmulap  8094  apmul1  8153  qapne  9019  divelunit  9314  modqid  9645  q2submod  9681  addmodlteq  9694  expadd  9834  leexp2r  9846  nnlesq  9894  sqoddm1div8  9941  nn0opthlem1d  9963  faclbnd  9984  faclbnd2  9985  faclbnd6  9987  facavg  9989  bcn0  9998  bcn1  10001  1dvds  10590  bezoutlema  10768  bezoutlemb  10769  gcdmultiple  10789  sqgcd  10798  lcm1  10843  coprmdvds  10854  qredeu  10859  phiprmpw  10978