Theorem mulridd 8195

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   1c1 8032   x. cmul 8036

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-mulcom 8132  ax-mulass 8134  ax-distr 8135  ax-1rid 8138  ax-cnre 8142

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  muladd11  8311  muls1d  8596  ltmul1  8771  mulap0  8833  divrecap  8867  diveqap1  8884  conjmulap  8908  apmul1  8967  qapne  9872  divelunit  10236  modqid  10610  q2submod  10646  addmodlteq  10659  expadd  10842  leexp2r  10854  nnlesq  10904  sqoddm1div8  10954  nn0opthlem1d  10981  faclbnd  11002  faclbnd2  11003  faclbnd6  11005  facavg  11007  bcn0  11016  bcn1  11019  reccn2ap  11873  hash2iun1dif1  12040  binom11  12046  trireciplem  12060  geosergap  12066  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  fprodsplitdc  12156  efzval  12243  tanaddaplem  12298  tanaddap  12299  cos01gt0  12323  absef  12330  1dvds  12365  bitsfzo  12515  bitsmod  12516  bezoutlema  12569  bezoutlemb  12570  gcdmultiple  12590  sqgcd  12599  lcm1  12652  coprmdvds  12663  qredeu  12668  phiprmpw  12793  coprimeprodsq  12829  pc2dvds  12902  sumhashdc  12919  fldivp1  12920  pcfaclem  12921  prmpwdvds  12927  zsssubrg  14598  mulgrhm2  14623  znrrg  14673  dveflem  15449  plyconst  15468  plycolemc  15481  efper  15530  tangtx  15561  logdivlti  15604  rpcxpmul2  15636  relogbexpap  15681  rplogbcxp  15686  0sgm  15708  lgsdir2  15761  lgsquad2lem1  15809  lgsquad3  15812  2sqlem6  15848  2sqlem8  15851  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  redcwlpolemeq1  16658  nconstwlpolemgt0  16668