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  8874  2mulicn  9477  numma  9770  nummac  9771  9t11e99  9856  decbin2  9867  irec  11025  binom2i  11034  3dec  11101  rei  11609  imi  11610  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  3lcm2e6woprm  12808  6lcm4e12  12809  modxai  13139  karatsuba  13153  ballotfilemth  13225  sinhalfpilem  15768  ef2pi  15782  ef2kpi  15783  efper  15784  sinperlem  15785  sin2kpi  15788  cos2kpi  15789  sin2pim  15790  cos2pim  15791  sincos4thpi  15817  sincos6thpi  15819  abssinper  15823  cosq34lt1  15827  lgsdir2lem5  16017  2lgsoddprmlem3c  16094  2lgsoddprmlem3d  16095