ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulcli Unicode version

Theorem mulcli 7997
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
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 mulcl 7973 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 426 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 2160  (class class class)co 5900   CCcc 7844    x. cmul 7851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 7944
This theorem is referenced by:  ixi  8575  2mulicn  9176  numma  9462  nummac  9463  9t11e99  9548  decbin2  9559  irec  10660  binom2i  10669  3dec  10735  rei  10949  imi  10950  3dvdsdec  11911  3dvds2dec  11912  odd2np1  11919  3lcm2e6woprm  12129  6lcm4e12  12130  sinhalfpilem  14697  ef2pi  14711  ef2kpi  14712  efper  14713  sinperlem  14714  sin2kpi  14717  cos2kpi  14718  sin2pim  14719  cos2pim  14720  sincos4thpi  14746  sincos6thpi  14748  abssinper  14752  cosq34lt1  14756  lgsdir2lem5  14919  2lgsoddprmlem3c  14943  2lgsoddprmlem3d  14944
  Copyright terms: Public domain W3C validator