Theorem mulcli 8050

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 8025	. 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 2167  (class class class)co 5925   CCcc 7896   x. cmul 7903

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

This theorem is referenced by:  ixi  8629  2mulicn  9232  numma  9519  nummac  9520  9t11e99  9605  decbin2  9616  irec  10750  binom2i  10759  3dec  10825  rei  11083  imi  11084  3dvdsdec  12049  3dvds2dec  12050  odd2np1  12057  3lcm2e6woprm  12281  6lcm4e12  12282  modxai  12612  karatsuba  12626  sinhalfpilem  15135  ef2pi  15149  ef2kpi  15150  efper  15151  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  sin2pim  15157  cos2pim  15158  sincos4thpi  15184  sincos6thpi  15186  abssinper  15190  cosq34lt1  15194  lgsdir2lem5  15381  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459