![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expimpd | Unicode version |
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
Ref | Expression |
---|---|
expimpd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
expimpd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expimpd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | impd 242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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: euotd 3982 swopo 4034 reusv3 4158 ralxfrd 4160 rexxfrd 4161 nlimsucg 4242 poirr2 4660 elpreima 5229 fmptco 5273 tposfo2 5823 nnm00 6038 th3qlem1 6144 recexprlemss1l 6607 recexprlemss1u 6608 cauappcvgprlemladdru 6628 cauappcvgprlemladdrl 6629 caucvgprlemladdrl 6649 uzind 8125 xltnegi 8518 ixxssixx 8541 expnegzap 8943 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |