Theorem mulridd 8089

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   1c1 7926   x. cmul 7930

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017  ax-1cn 8018  ax-icn 8020  ax-addcl 8021  ax-mulcl 8023  ax-mulcom 8026  ax-mulass 8028  ax-distr 8029  ax-1rid 8032  ax-cnre 8036

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  muladd11  8205  muls1d  8490  ltmul1  8665  mulap0  8727  divrecap  8761  diveqap1  8778  conjmulap  8802  apmul1  8861  qapne  9760  divelunit  10124  modqid  10494  q2submod  10530  addmodlteq  10543  expadd  10726  leexp2r  10738  nnlesq  10788  sqoddm1div8  10838  nn0opthlem1d  10865  faclbnd  10886  faclbnd2  10887  faclbnd6  10889  facavg  10891  bcn0  10900  bcn1  10903  reccn2ap  11624  hash2iun1dif1  11791  binom11  11797  trireciplem  11811  geosergap  11817  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  fprodsplitdc  11907  efzval  11994  tanaddaplem  12049  tanaddap  12050  cos01gt0  12074  absef  12081  1dvds  12116  bitsfzo  12266  bitsmod  12267  bezoutlema  12320  bezoutlemb  12321  gcdmultiple  12341  sqgcd  12350  lcm1  12403  coprmdvds  12414  qredeu  12419  phiprmpw  12544  coprimeprodsq  12580  pc2dvds  12653  sumhashdc  12670  fldivp1  12671  pcfaclem  12672  prmpwdvds  12678  zsssubrg  14347  mulgrhm2  14372  znrrg  14422  dveflem  15198  plyconst  15217  plycolemc  15230  efper  15279  tangtx  15310  logdivlti  15353  rpcxpmul2  15385  relogbexpap  15430  rplogbcxp  15435  0sgm  15457  lgsdir2  15510  lgsquad2lem1  15558  lgsquad3  15561  2sqlem6  15597  2sqlem8  15600  trilpolemclim  15975  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  redcwlpolemeq1  15993  nconstwlpolemgt0  16003