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  2491  reu6  2795  fun11iun  5239  poxp  5956  smoel  6021  iinerm  6318  suplub2ti  6643  infglbti  6667  infnlbti  6668  prarloclemlo  7000  peano5uzti  8790  lbzbi  9036  ssfzo12bi  9567  cau3lem  10446  isummo  10667  alzdvds  10761  nno  10812  nn0seqcvgd  10929  lcmdvds  10967  divgcdodd  11028
  Copyright terms: Public domain W3C validator