Theorem mulcli 8139

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 8114	. 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 2200  (class class class)co 5994   CCcc 7985   x. cmul 7992

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

This theorem is referenced by:  ixi  8718  2mulicn  9321  numma  9609  nummac  9610  9t11e99  9695  decbin2  9706  irec  10848  binom2i  10857  3dec  10923  rei  11396  imi  11397  3dvdsdec  12362  3dvds2dec  12363  odd2np1  12370  3lcm2e6woprm  12594  6lcm4e12  12595  modxai  12925  karatsuba  12939  sinhalfpilem  15450  ef2pi  15464  ef2kpi  15465  efper  15466  sinperlem  15467  sin2kpi  15470  cos2kpi  15471  sin2pim  15472  cos2pim  15473  sincos4thpi  15499  sincos6thpi  15501  abssinper  15505  cosq34lt1  15509  lgsdir2lem5  15696  2lgsoddprmlem3c  15773  2lgsoddprmlem3d  15774