Theorem mulcli 7590

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

Syntax hints:   e. wcel 1445  (class class class)co 5690   CCcc 7445   x. cmul 7452

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

This theorem is referenced by:  ixi  8157  2mulicn  8736  numma  9019  nummac  9020  9t11e99  9105  decbin2  9116  irec  10185  binom2i  10194  3dec  10254  rei  10464  imi  10465  3dvdsdec  11307  3dvds2dec  11308  odd2np1  11315  3lcm2e6woprm  11510  6lcm4e12  11511