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

Theorem exp32 347
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1
Assertion
Ref Expression
exp32

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3
21ex 108 . 2
32expd 245 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  exp44  355  exp45  356  expr  357  anassrs  380  an13s  501  3impb  1099  xordidc  1287  funfvima3  5335  isoini  5400  ovg  5581  fundmen  6222  distrlem1prl  6558  distrlem1pru  6559  recexgt0sr  6701  cnegexlem2  6984  mulgt1  7610
  Copyright terms: Public domain W3C validator