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  230  expt  646  hbimd  1552  moim  2063  moimv  2065  sstr2  3104  ssralv  3161  soss  4236  nneneq  6751  prarloclem3  7312  fzind  9173  exbtwnzlemshrink  10033  rebtwn2zlemshrink  10038  seq3fveq2  10249  seq3shft2  10253  monoord  10256  seq3split  10259  seq3id2  10289  seq3coll  10592  rexico  11000  cnntr  12404  setindft  13193
  Copyright terms: Public domain W3C validator