Theorem mulcli 8295

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 8270	. 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 2205  (class class class)co 6058   CCcc 8141   x. cmul 8148

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

This theorem is referenced by:  ixi  8875  2mulicn  9480  numma  9773  nummac  9774  9t11e99  9859  decbin2  9870  irec  11028  binom2i  11037  3dec  11104  rei  11613  imi  11614  3dvdsdec  12580  3dvds2dec  12581  odd2np1  12588  3lcm2e6woprm  12812  6lcm4e12  12813  modxai  13143  karatsuba  13157  ballotfilemth  13229  sinhalfpilem  15786  ef2pi  15800  ef2kpi  15801  efper  15802  sinperlem  15803  sin2kpi  15806  cos2kpi  15807  sin2pim  15808  cos2pim  15809  sincos4thpi  15835  sincos6thpi  15837  abssinper  15841  cosq34lt1  15845  lgsdir2lem5  16035  2lgsoddprmlem3c  16112  2lgsoddprmlem3d  16113