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  629  hbimd  1535  moim  2039  moimv  2041  sstr2  3072  ssralv  3129  soss  4204  nneneq  6717  prarloclem3  7269  fzind  9120  exbtwnzlemshrink  9977  rebtwn2zlemshrink  9982  seq3fveq2  10193  seq3shft2  10197  monoord  10200  seq3split  10203  seq3id2  10233  seq3coll  10536  rexico  10944  cnntr  12300  setindft  12997
  Copyright terms: Public domain W3C validator