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 4176 swopo 4228 reusv3 4381 ralxfrd 4383 rexxfrd 4384 nlimsucg 4481 poirr2 4931 elpreima 5539 fmptco 5586 tposfo2 6164 nnm00 6425 th3qlem1 6531 fiintim 6817 supmoti 6880 infglbti 6912 infnlbti 6913 updjud 6967 recexprlemss1l 7443 recexprlemss1u 7444 cauappcvgprlemladdru 7464 cauappcvgprlemladdrl 7465 caucvgprlemladdrl 7486 uzind 9162 ledivge1le 9513 xltnegi 9618 ixxssixx 9685 expnegzap 10327 shftlem 10588 cau3lem 10886 caubnd2 10889 climuni 11062 2clim 11070 summodclem2 11151 summodc 11152 zsumdc 11153 fsumf1o 11159 fisumss 11161 fsumcl2lem 11167 fsumadd 11175 fsummulc2 11217 prodmodclem2 11346 prodmodc 11347 dfgcd2 11702 cncongrprm 11835 eltg3 12226 tgidm 12243 tgrest 12338 tgcn 12377 lmtopcnp 12419 txbasval 12436 txcnp 12440 bldisj 12570 xblm 12586 blssps 12596 blss 12597 blssexps 12598 blssex 12599 metcnp3 12680 bj-findis 13177 |
Copyright terms: Public domain | W3C validator |