Theorem mulid1d 7878

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

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128  (class class class)co 5818   CCcc 7713   1c1 7716   x. cmul 7720

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7807  ax-1cn 7808  ax-icn 7810  ax-addcl 7811  ax-mulcl 7813  ax-mulcom 7816  ax-mulass 7818  ax-distr 7819  ax-1rid 7822  ax-cnre 7826

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-iota 5132  df-fv 5175  df-ov 5821

This theorem is referenced by:  muladd11  7991  ltmul1  8450  mulap0  8511  divrecap  8544  diveqap1  8561  conjmulap  8585  apmul1  8644  qapne  9530  divelunit  9888  modqid  10230  q2submod  10266  addmodlteq  10279  expadd  10443  leexp2r  10455  nnlesq  10504  sqoddm1div8  10553  nn0opthlem1d  10576  faclbnd  10597  faclbnd2  10598  faclbnd6  10600  facavg  10602  bcn0  10611  bcn1  10614  reccn2ap  11192  hash2iun1dif1  11359  binom11  11365  trireciplem  11379  geosergap  11385  cvgratnnlemnexp  11403  cvgratnnlemmn  11404  fprodsplitdc  11475  efzval  11562  tanaddaplem  11617  tanaddap  11618  cos01gt0  11641  absef  11648  1dvds  11682  bezoutlema  11863  bezoutlemb  11864  gcdmultiple  11884  sqgcd  11893  lcm1  11938  coprmdvds  11949  qredeu  11954  phiprmpw  12074  dveflem  13047  efper  13088  tangtx  13119  logdivlti  13162  relogbexpap  13235  rplogbcxp  13240  trilpolemclim  13569  trilpolemisumle  13571  trilpolemeq1  13573  trilpolemlt1  13574  redcwlpolemeq1  13587  nconstwlpolemgt0  13596