Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imim1d | Unicode 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 1561 moim 2078 moimv 2080 sstr2 3149 ssralv 3206 soss 4292 nneneq 6823 prarloclem3 7438 fzind 9306 exbtwnzlemshrink 10184 rebtwn2zlemshrink 10189 seq3fveq2 10404 seq3shft2 10408 monoord 10411 seq3split 10414 seq3id2 10444 seq3coll 10755 rexico 11163 cnntr 12865 2sqlem6 13596 setindft 13847 |
Copyright terms: Public domain | W3C validator |