Theorem mulridd 8119

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 8099	. 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 2177  (class class class)co 5962   CCcc 7953   1c1 7956   x. cmul 7960

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8047  ax-1cn 8048  ax-icn 8050  ax-addcl 8051  ax-mulcl 8053  ax-mulcom 8056  ax-mulass 8058  ax-distr 8059  ax-1rid 8062  ax-cnre 8066

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-iota 5246  df-fv 5293  df-ov 5965

This theorem is referenced by:  muladd11  8235  muls1d  8520  ltmul1  8695  mulap0  8757  divrecap  8791  diveqap1  8808  conjmulap  8832  apmul1  8891  qapne  9790  divelunit  10154  modqid  10526  q2submod  10562  addmodlteq  10575  expadd  10758  leexp2r  10770  nnlesq  10820  sqoddm1div8  10870  nn0opthlem1d  10897  faclbnd  10918  faclbnd2  10919  faclbnd6  10921  facavg  10923  bcn0  10932  bcn1  10935  reccn2ap  11709  hash2iun1dif1  11876  binom11  11882  trireciplem  11896  geosergap  11902  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  fprodsplitdc  11992  efzval  12079  tanaddaplem  12134  tanaddap  12135  cos01gt0  12159  absef  12166  1dvds  12201  bitsfzo  12351  bitsmod  12352  bezoutlema  12405  bezoutlemb  12406  gcdmultiple  12426  sqgcd  12435  lcm1  12488  coprmdvds  12499  qredeu  12504  phiprmpw  12629  coprimeprodsq  12665  pc2dvds  12738  sumhashdc  12755  fldivp1  12756  pcfaclem  12757  prmpwdvds  12763  zsssubrg  14432  mulgrhm2  14457  znrrg  14507  dveflem  15283  plyconst  15302  plycolemc  15315  efper  15364  tangtx  15395  logdivlti  15438  rpcxpmul2  15470  relogbexpap  15515  rplogbcxp  15520  0sgm  15542  lgsdir2  15595  lgsquad2lem1  15643  lgsquad3  15646  2sqlem6  15682  2sqlem8  15685  trilpolemclim  16147  trilpolemisumle  16149  trilpolemeq1  16151  trilpolemlt1  16152  redcwlpolemeq1  16165  nconstwlpolemgt0  16175