![]() |
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 2928 fun11iun 5484 poxp 6236 smoel 6304 iinerm 6610 suplub2ti 7003 infglbti 7027 infnlbti 7028 prarloclemlo 7496 peano5uzti 9364 lbzbi 9619 ssfzo12bi 10228 cau3lem 11126 summodc 11394 mertenslem2 11547 prodmodclem2 11588 alzdvds 11863 nno 11914 nn0seqcvgd 12044 lcmdvds 12082 divgcdodd 12146 prmpwdvds 12356 cnptoprest 13879 lmss 13886 txlm 13919 |
Copyright terms: Public domain | W3C validator |