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  652  hbimd  1566  moim  2083  moimv  2085  sstr2  3154  ssralv  3211  soss  4299  nneneq  6835  prarloclem3  7459  fzind  9327  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3id2  10465  seq3coll  10777  rexico  11185  cnntr  13019  2sqlem6  13750  setindft  14000
  Copyright terms: Public domain W3C validator