ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  expimpd 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  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
expimpd  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 108 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 242 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
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  3991  swopo  4043  reusv3  4192  ralxfrd  4194  rexxfrd  4195  nlimsucg  4290  poirr2  4717  elpreima  5286  fmptco  5330  tposfo2  5882  nnm00  6102  th3qlem1  6208  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  uzind  8349  ledivge1le  8652  xltnegi  8748  ixxssixx  8771  expnegzap  9289  shftlem  9417  cau3lem  9710  caubnd2  9713  climuni  9814  2clim  9822  bj-findis  10104
  Copyright terms: Public domain W3C validator