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

Theorem expimpd 345
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expimpd.1
Assertion
Ref Expression
expimpd

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3
21ex 108 . 2
32impd 242 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-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  euotd  3982  swopo  4034  reusv3  4158  ralxfrd  4160  rexxfrd  4161  nlimsucg  4242  poirr2  4660  elpreima  5229  fmptco  5273  tposfo2  5823  nnm00  6038  th3qlem1  6144  recexprlemss1l  6606  recexprlemss1u  6607  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  uzind  8105  xltnegi  8498  ixxssixx  8521  expnegzap  8923  bj-findis  9409
  Copyright terms: Public domain W3C validator