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 114 | . 2 |
3 | 2 | impd 252 | 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: euotd 4146 swopo 4198 reusv3 4351 ralxfrd 4353 rexxfrd 4354 nlimsucg 4451 poirr2 4901 elpreima 5507 fmptco 5554 tposfo2 6132 nnm00 6393 th3qlem1 6499 fiintim 6785 supmoti 6848 infglbti 6880 infnlbti 6881 updjud 6935 recexprlemss1l 7411 recexprlemss1u 7412 cauappcvgprlemladdru 7432 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 uzind 9120 ledivge1le 9468 xltnegi 9573 ixxssixx 9640 expnegzap 10282 shftlem 10543 cau3lem 10841 caubnd2 10844 climuni 11017 2clim 11025 summodclem2 11106 summodc 11107 zsumdc 11108 fsumf1o 11114 fisumss 11116 fsumcl2lem 11122 fsumadd 11130 fsummulc2 11172 dfgcd2 11614 cncongrprm 11747 eltg3 12137 tgidm 12154 tgrest 12249 tgcn 12288 lmtopcnp 12330 txbasval 12347 txcnp 12351 bldisj 12481 xblm 12497 blssps 12507 blss 12508 blssexps 12509 blssex 12510 metcnp3 12591 bj-findis 13073 |
Copyright terms: Public domain | W3C validator |