Theorem mulcli 8325

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

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC

Assertion

Ref	Expression
mulcli	|- ( A x. B ) e. CC

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		mulcl 8300	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) e. CC

Syntax hints:   e. wcel 2209  (class class class)co 6079   CCcc 8171   x. cmul 8178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8271

This theorem is referenced by:  ixi  8905  2mulicn  9510  numma  9803  nummac  9804  9t11e99  9889  decbin2  9900  irec  11059  binom2i  11068  3dec  11135  rei  11648  imi  11649  3dvdsdec  12615  3dvds2dec  12616  odd2np1  12623  3lcm2e6woprm  12847  6lcm4e12  12848  modxai  13178  karatsuba  13192  ballotfilemth  13264  sinhalfpilem  15875  ef2pi  15889  ef2kpi  15890  efper  15891  sinperlem  15892  sin2kpi  15895  cos2kpi  15896  sin2pim  15897  cos2pim  15898  sincos4thpi  15924  sincos6thpi  15926  abssinper  15930  cosq34lt1  15934  log2ublem2  16067  log2ublem3  16068  log2ublog2  16069  lgsdir2lem5  16134  2lgsoddprmlem3c  16211  2lgsoddprmlem3d  16212