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

Theorem imim1d 74
Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)
Hypothesis
Ref Expression
imim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imim1d  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )

Proof of Theorem imim1d
StepHypRef Expression
1 imim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2imim12d 73 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim1  75  imbi1d  229  expt  616  hbimd  1506  moim  2006  moimv  2008  sstr2  3007  ssralv  3059  soss  4077  nneneq  6392  prarloclem3  6749  fzind  8543  exbtwnzlemshrink  9335  rebtwn2zlemshrink  9340  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqid2  9564  rexico  10245  setindft  10918
  Copyright terms: Public domain W3C validator