Theorem mulridd 8088

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

Hypothesis

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

Assertion

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

Proof of Theorem mulridd

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

Syntax hints:   -> wi 4   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   1c1 7925   x. cmul 7929

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016  ax-1cn 8017  ax-icn 8019  ax-addcl 8020  ax-mulcl 8022  ax-mulcom 8025  ax-mulass 8027  ax-distr 8028  ax-1rid 8031  ax-cnre 8035

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  muladd11  8204  muls1d  8489  ltmul1  8664  mulap0  8726  divrecap  8760  diveqap1  8777  conjmulap  8801  apmul1  8860  qapne  9759  divelunit  10123  modqid  10492  q2submod  10528  addmodlteq  10541  expadd  10724  leexp2r  10736  nnlesq  10786  sqoddm1div8  10836  nn0opthlem1d  10863  faclbnd  10884  faclbnd2  10885  faclbnd6  10887  facavg  10889  bcn0  10898  bcn1  10901  reccn2ap  11595  hash2iun1dif1  11762  binom11  11768  trireciplem  11782  geosergap  11788  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  fprodsplitdc  11878  efzval  11965  tanaddaplem  12020  tanaddap  12021  cos01gt0  12045  absef  12052  1dvds  12087  bitsfzo  12237  bitsmod  12238  bezoutlema  12291  bezoutlemb  12292  gcdmultiple  12312  sqgcd  12321  lcm1  12374  coprmdvds  12385  qredeu  12390  phiprmpw  12515  coprimeprodsq  12551  pc2dvds  12624  sumhashdc  12641  fldivp1  12642  pcfaclem  12643  prmpwdvds  12649  zsssubrg  14318  mulgrhm2  14343  znrrg  14393  dveflem  15169  plyconst  15188  plycolemc  15201  efper  15250  tangtx  15281  logdivlti  15324  rpcxpmul2  15356  relogbexpap  15401  rplogbcxp  15406  0sgm  15428  lgsdir2  15481  lgsquad2lem1  15529  lgsquad3  15532  2sqlem6  15568  2sqlem8  15571  trilpolemclim  15937  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  redcwlpolemeq1  15955  nconstwlpolemgt0  15965