![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | impd 254 |
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: euotd 4250 swopo 4302 reusv3 4456 ralxfrd 4458 rexxfrd 4459 nlimsucg 4561 poirr2 5016 elpreima 5630 fmptco 5677 tposfo2 6261 nnm00 6524 th3qlem1 6630 fiintim 6921 supmoti 6985 infglbti 7017 infnlbti 7018 updjud 7074 recexprlemss1l 7612 recexprlemss1u 7613 cauappcvgprlemladdru 7633 cauappcvgprlemladdrl 7634 caucvgprlemladdrl 7655 uzind 9340 ledivge1le 9700 xltnegi 9809 ixxssixx 9876 expnegzap 10527 shftlem 10796 cau3lem 11094 caubnd2 11097 climuni 11272 2clim 11280 summodclem2 11361 summodc 11362 zsumdc 11363 fsumf1o 11369 fisumss 11371 fsumcl2lem 11377 fsumadd 11385 fsummulc2 11427 prodmodclem2 11556 prodmodc 11557 zproddc 11558 fprodf1o 11567 fprodssdc 11569 fprodmul 11570 dfgcd2 11985 cncongrprm 12127 prmpwdvds 12323 infpnlem1 12327 1arith 12335 isgrpid2 12790 dvdsrd 13075 dvdsrtr 13082 dvdsrmul1 13083 unitgrp 13097 eltg3 13190 tgidm 13207 tgrest 13302 tgcn 13341 lmtopcnp 13383 txbasval 13400 txcnp 13404 bldisj 13534 xblm 13550 blssps 13560 blss 13561 blssexps 13562 blssex 13563 metcnp3 13644 2sqlem6 14089 2sqlem7 14090 bj-findis 14353 |
Copyright terms: Public domain | W3C validator |