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  11566  hash2iun1dif1  11733  binom11  11739  trireciplem  11753  geosergap  11759  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  fprodsplitdc  11849  efzval  11936  tanaddaplem  11991  tanaddap  11992  cos01gt0  12016  absef  12023  1dvds  12058  bitsfzo  12208  bitsmod  12209  bezoutlema  12262  bezoutlemb  12263  gcdmultiple  12283  sqgcd  12292  lcm1  12345  coprmdvds  12356  qredeu  12361  phiprmpw  12486  coprimeprodsq  12522  pc2dvds  12595  sumhashdc  12612  fldivp1  12613  pcfaclem  12614  prmpwdvds  12620  zsssubrg  14289  mulgrhm2  14314  znrrg  14364  dveflem  15140  plyconst  15159  plycolemc  15172  efper  15221  tangtx  15252  logdivlti  15295  rpcxpmul2  15327  relogbexpap  15372  rplogbcxp  15377  0sgm  15399  lgsdir2  15452  lgsquad2lem1  15500  lgsquad3  15503  2sqlem6  15539  2sqlem8  15542  trilpolemclim  15908  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  redcwlpolemeq1  15926  nconstwlpolemgt0  15936