Theorem mulcli 7976

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 7952	. 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 2158  (class class class)co 5888   CCcc 7823   x. cmul 7830

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

This theorem is referenced by:  ixi  8554  2mulicn  9155  numma  9441  nummac  9442  9t11e99  9527  decbin2  9538  irec  10634  binom2i  10643  3dec  10708  rei  10922  imi  10923  3dvdsdec  11884  3dvds2dec  11885  odd2np1  11892  3lcm2e6woprm  12100  6lcm4e12  12101  sinhalfpilem  14508  ef2pi  14522  ef2kpi  14523  efper  14524  sinperlem  14525  sin2kpi  14528  cos2kpi  14529  sin2pim  14530  cos2pim  14531  sincos4thpi  14557  sincos6thpi  14559  abssinper  14563  cosq34lt1  14567  lgsdir2lem5  14729  2lgsoddprmlem3c  14753  2lgsoddprmlem3d  14754