![]() |
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 231 expt 657 hbimd 1573 moim 2090 moimv 2092 sstr2 3162 ssralv 3219 soss 4314 nneneq 6856 prarloclem3 7495 fzind 9367 exbtwnzlemshrink 10248 rebtwn2zlemshrink 10253 seq3fveq2 10468 seq3shft2 10472 monoord 10475 seq3split 10478 seq3id2 10508 seq3coll 10821 rexico 11229 cnntr 13695 2sqlem6 14437 setindft 14687 |
Copyright terms: Public domain | W3C validator |