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

Theorem mulcli 7175
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 7151 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 417 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1434  (class class class)co 5537   CCcc 7030    x. cmul 7037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcl 7125
This theorem is referenced by:  ixi  7739  2mulicn  8309  numma  8590  nummac  8591  9t11e99  8676  decbin2  8687  irec  9660  binom2i  9669  3dec  9728  rei  9913  imi  9914  3dvdsdec  10398  3dvds2dec  10399  odd2np1  10406  3lcm2e6woprm  10601  6lcm4e12  10602
  Copyright terms: Public domain W3C validator