Theorem mulcli 7958

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 7934	. 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 2148  (class class class)co 5871   CCcc 7805   x. cmul 7812

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

This theorem is referenced by:  ixi  8535  2mulicn  9136  numma  9422  nummac  9423  9t11e99  9508  decbin2  9519  irec  10613  binom2i  10622  3dec  10686  rei  10900  imi  10901  3dvdsdec  11861  3dvds2dec  11862  odd2np1  11869  3lcm2e6woprm  12077  6lcm4e12  12078  sinhalfpilem  14074  ef2pi  14088  ef2kpi  14089  efper  14090  sinperlem  14091  sin2kpi  14094  cos2kpi  14095  sin2pim  14096  cos2pim  14097  sincos4thpi  14123  sincos6thpi  14125  abssinper  14129  cosq34lt1  14133  lgsdir2lem5  14295