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  2928  fun11iun  5484  poxp  6236  smoel  6304  iinerm  6610  suplub2ti  7003  infglbti  7027  infnlbti  7028  prarloclemlo  7496  peano5uzti  9364  lbzbi  9619  ssfzo12bi  10228  cau3lem  11126  summodc  11394  mertenslem2  11547  prodmodclem2  11588  alzdvds  11863  nno  11914  nn0seqcvgd  12044  lcmdvds  12082  divgcdodd  12146  prmpwdvds  12356  cnptoprest  13879  lmss  13886  txlm  13919
  Copyright terms: Public domain W3C validator