Theorem mulcli 8084

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 8059	. 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 2177  (class class class)co 5951   CCcc 7930   x. cmul 7937

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

This theorem is referenced by:  ixi  8663  2mulicn  9266  numma  9554  nummac  9555  9t11e99  9640  decbin2  9651  irec  10791  binom2i  10800  3dec  10866  rei  11254  imi  11255  3dvdsdec  12220  3dvds2dec  12221  odd2np1  12228  3lcm2e6woprm  12452  6lcm4e12  12453  modxai  12783  karatsuba  12797  sinhalfpilem  15307  ef2pi  15321  ef2kpi  15322  efper  15323  sinperlem  15324  sin2kpi  15327  cos2kpi  15328  sin2pim  15329  cos2pim  15330  sincos4thpi  15356  sincos6thpi  15358  abssinper  15362  cosq34lt1  15366  lgsdir2lem5  15553  2lgsoddprmlem3c  15630  2lgsoddprmlem3d  15631