Theorem mulcli 8167

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 8142	. 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 6010   CCcc 8013   x. cmul 8020

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

This theorem is referenced by:  ixi  8746  2mulicn  9349  numma  9637  nummac  9638  9t11e99  9723  decbin2  9734  irec  10878  binom2i  10887  3dec  10953  rei  11431  imi  11432  3dvdsdec  12397  3dvds2dec  12398  odd2np1  12405  3lcm2e6woprm  12629  6lcm4e12  12630  modxai  12960  karatsuba  12974  sinhalfpilem  15486  ef2pi  15500  ef2kpi  15501  efper  15502  sinperlem  15503  sin2kpi  15506  cos2kpi  15507  sin2pim  15508  cos2pim  15509  sincos4thpi  15535  sincos6thpi  15537  abssinper  15541  cosq34lt1  15545  lgsdir2lem5  15732  2lgsoddprmlem3c  15809  2lgsoddprmlem3d  15810