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

Theorem expdimp 259
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expdimp  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem expdimp
StepHypRef Expression
1 exp3a.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21expd 258 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 124 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  rexlimdvv  2601  reu6  2926  fun11iun  5478  poxp  6227  smoel  6295  iinerm  6601  suplub2ti  6994  infglbti  7018  infnlbti  7019  prarloclemlo  7481  peano5uzti  9347  lbzbi  9602  ssfzo12bi  10208  cau3lem  11104  summodc  11372  mertenslem2  11525  prodmodclem2  11566  alzdvds  11840  nno  11891  nn0seqcvgd  12021  lcmdvds  12059  divgcdodd  12123  prmpwdvds  12333  cnptoprest  13403  lmss  13410  txlm  13443
  Copyright terms: Public domain W3C validator