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

Theorem expdimp 257
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 256 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 123 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  rexlimdvv  2531  reu6  2844  fun11iun  5354  poxp  6095  smoel  6163  iinerm  6467  suplub2ti  6854  infglbti  6878  infnlbti  6879  prarloclemlo  7266  peano5uzti  9113  lbzbi  9360  ssfzo12bi  9953  cau3lem  10837  summodc  11103  mertenslem2  11256  alzdvds  11459  nno  11510  nn0seqcvgd  11629  lcmdvds  11667  divgcdodd  11728  cnptoprest  12314  lmss  12321  txlm  12354
  Copyright terms: Public domain W3C validator