![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expdimp | Unicode version |
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |
Ref | Expression |
---|---|
exp3a.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
expdimp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp3a.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | expd 258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 124 |
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: rexlimdvv 2601 reu6 2926 fun11iun 5478 poxp 6227 smoel 6295 iinerm 6601 suplub2ti 6994 infglbti 7018 infnlbti 7019 prarloclemlo 7481 peano5uzti 9347 lbzbi 9602 ssfzo12bi 10208 cau3lem 11104 summodc 11372 mertenslem2 11525 prodmodclem2 11566 alzdvds 11840 nno 11891 nn0seqcvgd 12021 lcmdvds 12059 divgcdodd 12123 prmpwdvds 12333 cnptoprest 13403 lmss 13410 txlm 13443 |
Copyright terms: Public domain | W3C validator |