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  5482  poxp  6232  smoel  6300  iinerm  6606  suplub2ti  6999  infglbti  7023  infnlbti  7024  prarloclemlo  7492  peano5uzti  9360  lbzbi  9615  ssfzo12bi  10224  cau3lem  11122  summodc  11390  mertenslem2  11543  prodmodclem2  11584  alzdvds  11859  nno  11910  nn0seqcvgd  12040  lcmdvds  12078  divgcdodd  12142  prmpwdvds  12352  cnptoprest  13709  lmss  13716  txlm  13749
  Copyright terms: Public domain W3C validator