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 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 |