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

Theorem imim1d 75
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 74 1  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1  76  imbi1d  230  expt  647  hbimd  1561  moim  2078  moimv  2080  sstr2  3149  ssralv  3206  soss  4292  nneneq  6823  prarloclem3  7438  fzind  9306  exbtwnzlemshrink  10184  rebtwn2zlemshrink  10189  seq3fveq2  10404  seq3shft2  10408  monoord  10411  seq3split  10414  seq3id2  10444  seq3coll  10755  rexico  11163  cnntr  12865  2sqlem6  13596  setindft  13847
  Copyright terms: Public domain W3C validator