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 114 | . 2 |
3 | 2 | imp32 255 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: reximddv2 2537 moi2 2865 preq12bg 3700 ordsuc 4478 f1ocnv2d 5974 supisoti 6897 caucvgsrlemoffres 7608 prodge0 8612 un0addcl 9010 un0mulcl 9011 peano2uz2 9158 elfz2nn0 9892 fzind2 10016 expaddzap 10337 expmulzap 10339 cau3lem 10886 climuni 11062 climrecvg1n 11117 fisumcom2 11207 dvdsval2 11496 algcvga 11732 lcmgcdlem 11758 divgcdcoprmex 11783 epttop 12259 cncnp 12399 cnconst 12403 bl2in 12572 metcnpi 12684 metcnpi2 12685 metcnpi3 12686 |
Copyright terms: Public domain | W3C validator |