Theorem mulridd 8349

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   1c1 8186   x. cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-mulcom 8286  ax-mulass 8288  ax-distr 8289  ax-1rid 8292  ax-cnre 8296

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  muladd11  8466  muls1d  8752  ltmul1  8928  mulap0  8990  divrecap  9026  diveqap1  9043  conjmulap  9067  apmul1  9126  qapne  10054  divelunit  10420  modqid  10806  q2submod  10842  addmodlteq  10855  expadd  11038  leexp2r  11050  nnlesq  11100  sqoddm1div8  11151  nn0opthlem1d  11179  faclbnd  11200  faclbnd2  11201  faclbnd6  11203  facavg  11205  bcn0  11214  bcn1  11217  hashf1lem2  11307  hashfac  11309  reccn2ap  12103  hash2iun1dif1  12271  binom11  12277  trireciplem  12291  geosergap  12297  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  fprodsplitdc  12387  efzval  12474  tanaddaplem  12529  tanaddap  12530  cos01gt0  12554  absef  12561  1dvds  12596  bitsfzo  12746  bitsmod  12747  bezoutlema  12800  bezoutlemb  12801  gcdmultiple  12821  sqgcd  12830  lcm1  12883  coprmdvds  12894  qredeu  12899  phiprmpw  13028  coprimeprodsq  13064  pc2dvds  13137  sumhashdc  13154  fldivp1  13155  pcfaclem  13156  prmpwdvds  13162  zsssubrg  15030  mulgrhm2  15053  znrrg  15103  dveflem  15969  plyconst  15988  plycolemc  16001  efper  16051  tangtx  16082  logdivlti  16128  logdivlt  16141  rpcxpmul2  16163  efnthr  16193  relogbexpap  16211  rplogbcxp  16216  birthdaylem3  16244  0sgm  16271  bposlem1  16328  bposlem2  16329  bposlem5  16332  lgsdir2  16374  lgsquad2lem1  16422  lgsquad3  16425  2sqlem6  16461  2sqlem8  16464  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  redcwlpolemeq1  17328  nconstwlpolemgt0  17338