Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imim1d | GIF version |
Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.) |
Ref | Expression |
---|---|
imim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
imim1d | ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | idd 21 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
3 | 1, 2 | imim12d 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 652 hbimd 1566 moim 2083 moimv 2085 sstr2 3154 ssralv 3211 soss 4299 nneneq 6835 prarloclem3 7459 fzind 9327 exbtwnzlemshrink 10205 rebtwn2zlemshrink 10210 seq3fveq2 10425 seq3shft2 10429 monoord 10432 seq3split 10435 seq3id2 10465 seq3coll 10777 rexico 11185 cnntr 13019 2sqlem6 13750 setindft 14000 |
Copyright terms: Public domain | W3C validator |