Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impr | Unicode version |
Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
impr.1 |
Ref | Expression |
---|---|
impr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impr.1 | . . 3 | |
2 | 1 | ex 108 | . 2 |
3 | 2 | imp32 244 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: moi2 2722 preq12bg 3544 ordsuc 4287 f1ocnv2d 5704 caucvgsrlemoffres 6884 prodge0 7820 un0addcl 8215 un0mulcl 8216 peano2uz2 8345 elfz2nn0 8973 fzind2 9095 expaddzap 9299 expmulzap 9301 cau3lem 9710 climuni 9814 climrecvg1n 9867 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |