Theorem mulcli 7937

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 7913	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	mp2an 426	1 |- ( A x. B ) e. CC

Syntax hints:   e. wcel 2146  (class class class)co 5865   CCcc 7784   x. cmul 7791

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

This theorem is referenced by:  ixi  8514  2mulicn  9114  numma  9400  nummac  9401  9t11e99  9486  decbin2  9497  irec  10589  binom2i  10598  3dec  10662  rei  10876  imi  10877  3dvdsdec  11837  3dvds2dec  11838  odd2np1  11845  3lcm2e6woprm  12053  6lcm4e12  12054  sinhalfpilem  13783  ef2pi  13797  ef2kpi  13798  efper  13799  sinperlem  13800  sin2kpi  13803  cos2kpi  13804  sin2pim  13805  cos2pim  13806  sincos4thpi  13832  sincos6thpi  13834  abssinper  13838  cosq34lt1  13842  lgsdir2lem5  14004