Theorem mulcli 8227

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 8202	. 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 2202  (class class class)co 6028   CCcc 8073   x. cmul 8080

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

This theorem is referenced by:  ixi  8806  2mulicn  9409  numma  9697  nummac  9698  9t11e99  9783  decbin2  9794  irec  10945  binom2i  10954  3dec  11020  rei  11520  imi  11521  3dvdsdec  12487  3dvds2dec  12488  odd2np1  12495  3lcm2e6woprm  12719  6lcm4e12  12720  modxai  13050  karatsuba  13064  sinhalfpilem  15582  ef2pi  15596  ef2kpi  15597  efper  15598  sinperlem  15599  sin2kpi  15602  cos2kpi  15603  sin2pim  15604  cos2pim  15605  sincos4thpi  15631  sincos6thpi  15633  abssinper  15637  cosq34lt1  15641  lgsdir2lem5  15831  2lgsoddprmlem3c  15908  2lgsoddprmlem3d  15909