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 646 hbimd 1552 moim 2063 moimv 2065 sstr2 3104 ssralv 3161 soss 4236 nneneq 6751 prarloclem3 7305 fzind 9166 exbtwnzlemshrink 10026 rebtwn2zlemshrink 10031 seq3fveq2 10242 seq3shft2 10246 monoord 10249 seq3split 10252 seq3id2 10282 seq3coll 10585 rexico 10993 cnntr 12394 setindft 13163 |
Copyright terms: Public domain | W3C validator |