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  618  hbimd  1510  moim  2012  moimv  2014  sstr2  3030  ssralv  3083  soss  4132  nneneq  6553  prarloclem3  7035  fzind  8831  exbtwnzlemshrink  9625  rebtwn2zlemshrink  9630  iseqfveq2  9855  seq3fveq2  9857  iseqshft2  9863  monoord  9869  seq3split  9872  iseqsplit  9873  seq3id2  9905  iseqid2  9906  iseqcoll  10212  rexico  10619  setindft  11517
  Copyright terms: Public domain W3C validator