Theorem mulcli 8278

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 8253	. 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 2203  (class class class)co 6049   CCcc 8124   x. cmul 8131

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

This theorem is referenced by:  ixi  8856  2mulicn  9459  numma  9751  nummac  9752  9t11e99  9837  decbin2  9848  irec  11000  binom2i  11009  3dec  11075  rei  11580  imi  11581  3dvdsdec  12547  3dvds2dec  12548  odd2np1  12555  3lcm2e6woprm  12779  6lcm4e12  12780  modxai  13110  karatsuba  13124  sinhalfpilem  15648  ef2pi  15662  ef2kpi  15663  efper  15664  sinperlem  15665  sin2kpi  15668  cos2kpi  15669  sin2pim  15670  cos2pim  15671  sincos4thpi  15697  sincos6thpi  15699  abssinper  15703  cosq34lt1  15707  lgsdir2lem5  15897  2lgsoddprmlem3c  15974  2lgsoddprmlem3d  15975