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

Theorem expdimp 255
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 254 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 122 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:  rexlimdvv  2484  reu6  2782  fun11iun  5178  poxp  5884  smoel  5949  iinerm  6244  suplub2ti  6473  infglbti  6497  infnlbti  6498  prarloclemlo  6746  peano5uzti  8536  lbzbi  8782  ssfzo12bi  9311  cau3lem  10138  alzdvds  10399  nno  10450  nn0seqcvgd  10567  lcmdvds  10605  divgcdodd  10666
  Copyright terms: Public domain W3C validator