Theorem mulcli 8184

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 8159	. 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 6018   CCcc 8030   x. cmul 8037

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

This theorem is referenced by:  ixi  8763  2mulicn  9366  numma  9654  nummac  9655  9t11e99  9740  decbin2  9751  irec  10902  binom2i  10911  3dec  10977  rei  11464  imi  11465  3dvdsdec  12431  3dvds2dec  12432  odd2np1  12439  3lcm2e6woprm  12663  6lcm4e12  12664  modxai  12994  karatsuba  13008  sinhalfpilem  15521  ef2pi  15535  ef2kpi  15536  efper  15537  sinperlem  15538  sin2kpi  15541  cos2kpi  15542  sin2pim  15543  cos2pim  15544  sincos4thpi  15570  sincos6thpi  15572  abssinper  15576  cosq34lt1  15580  lgsdir2lem5  15767  2lgsoddprmlem3c  15844  2lgsoddprmlem3d  15845