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

Theorem imim1d 73
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 72 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  74  imbi1d  224  expt  593  hbimd  1481  moim  1980  moimv  1982  sstr2  2980  ssralv  3032  soss  4079  nneneq  6351  prarloclem3  6653  fzind  8412  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  setindft  10477
  Copyright terms: Public domain W3C validator