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

Proof of Theorem imim1d
StepHypRef Expression
1 imim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 21 . 2 (𝜑 → (𝜃𝜃))
31, 2imim12d 73 1 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
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  9854  seq3fveq2  9856  iseqshft2  9862  monoord  9869  seq3split  9872  iseqsplit  9873  iseqid2  9905  iseqcoll  10211  rexico  10618  setindft  11504
  Copyright terms: Public domain W3C validator