ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim1d GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imim1d (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))

Proof of Theorem imim1d
StepHypRef Expression
1 imim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 21 . 2 (𝜑 → (𝜃𝜃))
31, 2imim12d 74 1 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
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  231  expt  657  hbimd  1573  moim  2090  moimv  2092  sstr2  3162  ssralv  3219  soss  4314  nneneq  6856  prarloclem3  7495  fzind  9367  exbtwnzlemshrink  10248  rebtwn2zlemshrink  10253  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  seq3id2  10508  seq3coll  10821  rexico  11229  cnntr  13695  2sqlem6  14437  setindft  14687
  Copyright terms: Public domain W3C validator