![]() |
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 5482 poxp 6232 smoel 6300 iinerm 6606 suplub2ti 6999 infglbti 7023 infnlbti 7024 prarloclemlo 7492 peano5uzti 9360 lbzbi 9615 ssfzo12bi 10224 cau3lem 11122 summodc 11390 mertenslem2 11543 prodmodclem2 11584 alzdvds 11859 nno 11910 nn0seqcvgd 12040 lcmdvds 12078 divgcdodd 12142 prmpwdvds 12352 cnptoprest 13709 lmss 13716 txlm 13749 |
Copyright terms: Public domain | W3C validator |