Theorem mulcli 7997

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 7973	. 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 2160  (class class class)co 5900   CCcc 7844   x. cmul 7851

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

This theorem is referenced by:  ixi  8575  2mulicn  9176  numma  9462  nummac  9463  9t11e99  9548  decbin2  9559  irec  10660  binom2i  10669  3dec  10735  rei  10949  imi  10950  3dvdsdec  11911  3dvds2dec  11912  odd2np1  11919  3lcm2e6woprm  12129  6lcm4e12  12130  sinhalfpilem  14697  ef2pi  14711  ef2kpi  14712  efper  14713  sinperlem  14714  sin2kpi  14717  cos2kpi  14718  sin2pim  14719  cos2pim  14720  sincos4thpi  14746  sincos6thpi  14748  abssinper  14752  cosq34lt1  14756  lgsdir2lem5  14919  2lgsoddprmlem3c  14943  2lgsoddprmlem3d  14944