Theorem mulcli 8177

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 8152	. 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 6013   CCcc 8023   x. cmul 8030

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

This theorem is referenced by:  ixi  8756  2mulicn  9359  numma  9647  nummac  9648  9t11e99  9733  decbin2  9744  irec  10894  binom2i  10903  3dec  10969  rei  11453  imi  11454  3dvdsdec  12419  3dvds2dec  12420  odd2np1  12427  3lcm2e6woprm  12651  6lcm4e12  12652  modxai  12982  karatsuba  12996  sinhalfpilem  15508  ef2pi  15522  ef2kpi  15523  efper  15524  sinperlem  15525  sin2kpi  15528  cos2kpi  15529  sin2pim  15530  cos2pim  15531  sincos4thpi  15557  sincos6thpi  15559  abssinper  15563  cosq34lt1  15567  lgsdir2lem5  15754  2lgsoddprmlem3c  15831  2lgsoddprmlem3d  15832