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 2575 moi2 2911 preq12bg 3758 ordsuc 4545 f1ocnv2d 6050 supisoti 6983 caucvgsrlemoffres 7749 prodge0 8757 un0addcl 9155 un0mulcl 9156 peano2uz2 9306 elfz2nn0 10055 fzind2 10182 expaddzap 10507 expmulzap 10509 cau3lem 11065 climuni 11243 climrecvg1n 11298 fisumcom2 11388 fprodcom2fi 11576 dvdsval2 11739 algcvga 11992 lcmgcdlem 12018 divgcdcoprmex 12043 prmpwdvds 12294 epttop 12805 cncnp 12945 cnconst 12949 bl2in 13118 metcnpi 13230 metcnpi2 13231 metcnpi3 13232 |
Copyright terms: Public domain | W3C validator |