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

Theorem mulcli 7739
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 7715 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 422 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1465  (class class class)co 5742   CCcc 7586    x. cmul 7593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7686
This theorem is referenced by:  ixi  8313  2mulicn  8910  numma  9193  nummac  9194  9t11e99  9279  decbin2  9290  irec  10360  binom2i  10369  3dec  10429  rei  10639  imi  10640  3dvdsdec  11489  3dvds2dec  11490  odd2np1  11497  3lcm2e6woprm  11694  6lcm4e12  11695  sinhalfpilem  12799  ef2pi  12813  ef2kpi  12814  efper  12815  sinperlem  12816  sin2kpi  12819  cos2kpi  12820  sin2pim  12821  cos2pim  12822  sincos4thpi  12848  sincos6thpi  12850  abssinper  12854  cosq34lt1  12858
  Copyright terms: Public domain W3C validator