Theorem mulridd 8343

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 8323	. 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 6085   CCcc 8177   1c1 8180   x. cmul 8184

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 8271  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-mulcom 8280  ax-mulass 8282  ax-distr 8283  ax-1rid 8286  ax-cnre 8290

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  muladd11  8459  muls1d  8745  ltmul1  8920  mulap0  8982  divrecap  9018  diveqap1  9035  conjmulap  9059  apmul1  9118  qapne  10039  divelunit  10404  modqid  10786  q2submod  10822  addmodlteq  10835  expadd  11018  leexp2r  11030  nnlesq  11080  sqoddm1div8  11131  nn0opthlem1d  11158  faclbnd  11179  faclbnd2  11180  faclbnd6  11182  facavg  11184  bcn0  11193  bcn1  11196  hashf1lem2  11286  hashfac  11288  reccn2ap  12079  hash2iun1dif1  12247  binom11  12253  trireciplem  12267  geosergap  12273  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  fprodsplitdc  12363  efzval  12450  tanaddaplem  12505  tanaddap  12506  cos01gt0  12530  absef  12537  1dvds  12572  bitsfzo  12722  bitsmod  12723  bezoutlema  12776  bezoutlemb  12777  gcdmultiple  12797  sqgcd  12806  lcm1  12859  coprmdvds  12870  qredeu  12875  phiprmpw  13000  coprimeprodsq  13036  pc2dvds  13109  sumhashdc  13126  fldivp1  13127  pcfaclem  13128  prmpwdvds  13134  zsssubrg  14922  mulgrhm2  14945  znrrg  14995  dveflem  15827  plyconst  15846  plycolemc  15859  efper  15908  tangtx  15939  logdivlti  15982  rpcxpmul2  16015  relogbexpap  16060  rplogbcxp  16065  birthdaylem3  16089  0sgm  16099  lgsdir2  16152  lgsquad2lem1  16200  lgsquad3  16203  2sqlem6  16239  2sqlem8  16242  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  redcwlpolemeq1  17104  nconstwlpolemgt0  17114