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  647  hbimd  1553  moim  2070  moimv  2072  sstr2  3135  ssralv  3192  soss  4274  nneneq  6802  prarloclem3  7417  fzind  9279  exbtwnzlemshrink  10148  rebtwn2zlemshrink  10153  seq3fveq2  10368  seq3shft2  10372  monoord  10375  seq3split  10378  seq3id2  10408  seq3coll  10713  rexico  11121  cnntr  12625  setindft  13540
  Copyright terms: Public domain W3C validator