Theorem mulcli 8159

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 8134	. 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 2200  (class class class)co 6007   CCcc 8005   x. cmul 8012

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

This theorem is referenced by:  ixi  8738  2mulicn  9341  numma  9629  nummac  9630  9t11e99  9715  decbin2  9726  irec  10869  binom2i  10878  3dec  10944  rei  11418  imi  11419  3dvdsdec  12384  3dvds2dec  12385  odd2np1  12392  3lcm2e6woprm  12616  6lcm4e12  12617  modxai  12947  karatsuba  12961  sinhalfpilem  15473  ef2pi  15487  ef2kpi  15488  efper  15489  sinperlem  15490  sin2kpi  15493  cos2kpi  15494  sin2pim  15495  cos2pim  15496  sincos4thpi  15522  sincos6thpi  15524  abssinper  15528  cosq34lt1  15532  lgsdir2lem5  15719  2lgsoddprmlem3c  15796  2lgsoddprmlem3d  15797