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

Theorem expimpd 355
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 113 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 251 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  euotd  4017  swopo  4069  reusv3  4218  ralxfrd  4220  rexxfrd  4221  nlimsucg  4317  poirr2  4747  elpreima  5318  fmptco  5362  tposfo2  5916  nnm00  6168  th3qlem1  6274  supmoti  6465  infglbti  6497  infnlbti  6498  recexprlemss1l  6887  recexprlemss1u  6888  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemladdrl  6930  uzind  8539  ledivge1le  8884  xltnegi  8978  ixxssixx  9001  expnegzap  9607  shftlem  9842  cau3lem  10138  caubnd2  10141  climuni  10270  2clim  10278  dfgcd2  10547  cncongrprm  10680  bj-findis  10959
  Copyright terms: Public domain W3C validator