Theorem mulcli 7771

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

Syntax hints:   e. wcel 1480  (class class class)co 5774   CCcc 7618   x. cmul 7625

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

This theorem is referenced by:  ixi  8345  2mulicn  8942  numma  9225  nummac  9226  9t11e99  9311  decbin2  9322  irec  10392  binom2i  10401  3dec  10461  rei  10671  imi  10672  3dvdsdec  11562  3dvds2dec  11563  odd2np1  11570  3lcm2e6woprm  11767  6lcm4e12  11768  sinhalfpilem  12872  ef2pi  12886  ef2kpi  12887  efper  12888  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  sin2pim  12894  cos2pim  12895  sincos4thpi  12921  sincos6thpi  12923  abssinper  12927  cosq34lt1  12931