Theorem mulcli 9622

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1
axi.2

Assertion

Ref	Expression
mulcli

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2
2		axi.2	. 2
3		mulcl 9597	. 2
4	1, 2, 3	mp2an 672	1

Syntax hints:  e.wcel 1818  (class class class)co 6296  cc 9511  cmul 9518

This theorem is referenced by:  mul02lem2  9778  addid1  9781  cnegex2  9783  ixi  10203  2mulicn  10787  numma  11035  nummac  11036  decbin2  11108  irec  12267  binom2i  12277  binom2aiOLD  12278  crreczi  12291  nn0opthi  12350  faclbnd4lem1  12371  rei  12989  imi  12990  iseraltlem2  13505  odd2np1  14046  gcdaddmlem  14166  modxai  14554  mod2xnegi  14557  decexp2  14561  decsplit  14569  karatsuba  14570  sinhalfpilem  22856  ef2pi  22870  ef2kpi  22871  efper  22872  sinperlem  22873  sin2kpi  22876  cos2kpi  22877  sin2pim  22878  cos2pim  22879  sincos4thpi  22906  sincos6thpi  22908  pige3  22910  abssinper  22911  efeq1  22916  logneg  22972  logm1  22973  eflogeq  22986  logimul  22999  logneg2  23000  cxpsqrt  23084  root1eq1  23129  cxpeq  23131  ang180lem1  23141  ang180lem3  23143  ang180lem4  23144  1cubrlem  23172  1cubr  23173  quart1lem  23186  asin1  23225  atanlogsublem  23246  log2ublem2  23278  log2ublem3  23279  log2ub  23280  bclbnd  23555  bposlem8  23566  bposlem9  23567  lgsdir2lem5  23602  ax5seglem7  24238  ip0i  25740  ip1ilem  25741  ipasslem10  25754  siilem1  25766  normlem0  26026  normlem1  26027  normlem2  26028  normlem3  26029  normlem5  26031  normlem7  26033  bcseqi  26037  norm-ii-i  26054  normpar2i  26073  polid2i  26074  h1de2i  26471  lnopunilem1  26929  lnophmlem2  26936  ballotth  28476  problem2  29020  problem4  29022  quad3  29024  logi  29121  bpoly3  29820  bpoly4  29821  heiborlem6  30312  proot1ex  31161  areaquad  31184  coskpi2  31666  cosnegpi  31667  cosknegpi  31669  wallispilem4  31850  dirkerper  31878  dirkertrigeq  31883  dirkercncflem2  31886  fourierdlem57  31946  fourierdlem62  31951  fourierswlem  32013  zlmodzxzequap  33100  i2linesi  33193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9575

This theorem depends on definitions:  df-bi 185  df-an 371