Theorem mulcli 7962

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 7938	. 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 2148  (class class class)co 5875   CCcc 7809   x. cmul 7816

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

This theorem is referenced by:  ixi  8540  2mulicn  9141  numma  9427  nummac  9428  9t11e99  9513  decbin2  9524  irec  10620  binom2i  10629  3dec  10694  rei  10908  imi  10909  3dvdsdec  11870  3dvds2dec  11871  odd2np1  11878  3lcm2e6woprm  12086  6lcm4e12  12087  sinhalfpilem  14215  ef2pi  14229  ef2kpi  14230  efper  14231  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  sin2pim  14237  cos2pim  14238  sincos4thpi  14264  sincos6thpi  14266  abssinper  14270  cosq34lt1  14274  lgsdir2lem5  14436  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461