Theorem mulcli 7175

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

Syntax hints:   e. wcel 1434  (class class class)co 5537   CCcc 7030   x. cmul 7037

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

This theorem is referenced by:  ixi  7739  2mulicn  8309  numma  8590  nummac  8591  9t11e99  8676  decbin2  8687  irec  9660  binom2i  9669  3dec  9728  rei  9913  imi  9914  3dvdsdec  10398  3dvds2dec  10399  odd2np1  10406  3lcm2e6woprm  10601  6lcm4e12  10602