![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp32 257 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: reximddv2 2582 moi2 2920 preq12bg 3775 ordsuc 4564 f1ocnv2d 6078 supisoti 7012 caucvgsrlemoffres 7802 prodge0 8814 un0addcl 9212 un0mulcl 9213 peano2uz2 9363 elfz2nn0 10115 fzind2 10242 expaddzap 10567 expmulzap 10569 cau3lem 11126 climuni 11304 climrecvg1n 11359 fisumcom2 11449 fprodcom2fi 11637 dvdsval2 11800 algcvga 12054 lcmgcdlem 12080 divgcdcoprmex 12105 prmpwdvds 12356 isgrpinv 12935 dvdsrcl2 13306 islss4 13507 lspsnel6 13533 epttop 13778 cncnp 13918 cnconst 13922 bl2in 14091 metcnpi 14203 metcnpi2 14204 metcnpi3 14205 |
Copyright terms: Public domain | W3C validator |