![]() |
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 658 hbimd 1584 moim 2106 moimv 2108 sstr2 3187 ssralv 3244 soss 4346 nneneq 6915 prarloclem3 7559 fzind 9435 exbtwnzlemshrink 10320 rebtwn2zlemshrink 10325 seq3fveq2 10549 seqfveq2g 10551 seq3shft2 10555 seqshft2g 10556 monoord 10559 seq3split 10562 seqsplitg 10563 seq3id2 10600 seqhomog 10604 seq3coll 10916 rexico 11368 cnntr 14404 2sqlem6 15277 setindft 15527 |
Copyright terms: Public domain | W3C validator |