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

Theorem mulcli 7778
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 7754 . 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 1480  (class class class)co 5774   CCcc 7625    x. cmul 7632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7725
This theorem is referenced by:  ixi  8352  2mulicn  8949  numma  9232  nummac  9233  9t11e99  9318  decbin2  9329  irec  10399  binom2i  10408  3dec  10468  rei  10678  imi  10679  3dvdsdec  11569  3dvds2dec  11570  odd2np1  11577  3lcm2e6woprm  11774  6lcm4e12  11775  sinhalfpilem  12885  ef2pi  12899  ef2kpi  12900  efper  12901  sinperlem  12902  sin2kpi  12905  cos2kpi  12906  sin2pim  12907  cos2pim  12908  sincos4thpi  12934  sincos6thpi  12936  abssinper  12940  cosq34lt1  12944
  Copyright terms: Public domain W3C validator