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  4057  swopo  4109  reusv3  4258  ralxfrd  4260  rexxfrd  4261  nlimsucg  4357  poirr2  4793  elpreima  5383  fmptco  5429  tposfo2  5988  nnm00  6242  th3qlem1  6348  supmoti  6635  infglbti  6667  infnlbti  6668  updjud  6720  recexprlemss1l  7141  recexprlemss1u  7142  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprlemladdrl  7184  uzind  8793  ledivge1le  9138  xltnegi  9232  ixxssixx  9255  expnegzap  9891  shftlem  10150  cau3lem  10446  caubnd2  10449  climuni  10579  2clim  10587  isummolem2  10666  isummo  10667  zisum  10668  fsumf1o  10673  fisumss  10675  fsumcl2lem  10680  fsumadd  10688  dfgcd2  10909  cncongrprm  11042  bj-findis  11343
  Copyright terms: Public domain W3C validator