Theorem mulridd 8291

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   1c1 8128   x. cmul 8132

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-mulcom 8228  ax-mulass 8230  ax-distr 8231  ax-1rid 8234  ax-cnre 8238

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  muladd11  8406  muls1d  8691  ltmul1  8866  mulap0  8928  divrecap  8962  diveqap1  8979  conjmulap  9003  apmul1  9062  qapne  9971  divelunit  10335  modqid  10711  q2submod  10747  addmodlteq  10760  expadd  10943  leexp2r  10955  nnlesq  11005  sqoddm1div8  11055  nn0opthlem1d  11082  faclbnd  11103  faclbnd2  11104  faclbnd6  11106  facavg  11108  bcn0  11117  bcn1  11120  reccn2ap  11998  hash2iun1dif1  12166  binom11  12172  trireciplem  12186  geosergap  12192  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  fprodsplitdc  12282  efzval  12369  tanaddaplem  12424  tanaddap  12425  cos01gt0  12449  absef  12456  1dvds  12491  bitsfzo  12641  bitsmod  12642  bezoutlema  12695  bezoutlemb  12696  gcdmultiple  12716  sqgcd  12725  lcm1  12778  coprmdvds  12789  qredeu  12794  phiprmpw  12919  coprimeprodsq  12955  pc2dvds  13028  sumhashdc  13045  fldivp1  13046  pcfaclem  13047  prmpwdvds  13053  zsssubrg  14733  mulgrhm2  14758  znrrg  14808  dveflem  15591  plyconst  15610  plycolemc  15623  efper  15672  tangtx  15703  logdivlti  15746  rpcxpmul2  15778  relogbexpap  15823  rplogbcxp  15828  0sgm  15853  lgsdir2  15906  lgsquad2lem1  15954  lgsquad3  15957  2sqlem6  15993  2sqlem8  15996  trilpolemclim  16820  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  redcwlpolemeq1  16839  nconstwlpolemgt0  16850