Theorem mulcli 8090

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 8065	. 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 2177  (class class class)co 5954   CCcc 7936   x. cmul 7943

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

This theorem is referenced by:  ixi  8669  2mulicn  9272  numma  9560  nummac  9561  9t11e99  9646  decbin2  9657  irec  10797  binom2i  10806  3dec  10872  rei  11260  imi  11261  3dvdsdec  12226  3dvds2dec  12227  odd2np1  12234  3lcm2e6woprm  12458  6lcm4e12  12459  modxai  12789  karatsuba  12803  sinhalfpilem  15313  ef2pi  15327  ef2kpi  15328  efper  15329  sinperlem  15330  sin2kpi  15333  cos2kpi  15334  sin2pim  15335  cos2pim  15336  sincos4thpi  15362  sincos6thpi  15364  abssinper  15368  cosq34lt1  15372  lgsdir2lem5  15559  2lgsoddprmlem3c  15636  2lgsoddprmlem3d  15637