Theorem mulcli 7795

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

Syntax hints:   e. wcel 1481  (class class class)co 5782   CCcc 7642   x. cmul 7649

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

This theorem is referenced by:  ixi  8369  2mulicn  8966  numma  9249  nummac  9250  9t11e99  9335  decbin2  9346  irec  10423  binom2i  10432  3dec  10492  rei  10703  imi  10704  3dvdsdec  11598  3dvds2dec  11599  odd2np1  11606  3lcm2e6woprm  11803  6lcm4e12  11804  sinhalfpilem  12920  ef2pi  12934  ef2kpi  12935  efper  12936  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  sin2pim  12942  cos2pim  12943  sincos4thpi  12969  sincos6thpi  12971  abssinper  12975  cosq34lt1  12979