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 1553 moim 2070 moimv 2072 sstr2 3135 ssralv 3192 soss 4276 nneneq 6804 prarloclem3 7419 fzind 9284 exbtwnzlemshrink 10157 rebtwn2zlemshrink 10162 seq3fveq2 10377 seq3shft2 10381 monoord 10384 seq3split 10387 seq3id2 10417 seq3coll 10724 rexico 11132 cnntr 12695 setindft 13611 |
Copyright terms: Public domain | W3C validator |