![]() |
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 256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 123 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: rexlimdvv 2559 reu6 2877 fun11iun 5396 poxp 6137 smoel 6205 iinerm 6509 suplub2ti 6896 infglbti 6920 infnlbti 6921 prarloclemlo 7326 peano5uzti 9183 lbzbi 9435 ssfzo12bi 10033 cau3lem 10918 summodc 11184 mertenslem2 11337 prodmodclem2 11378 alzdvds 11588 nno 11639 nn0seqcvgd 11758 lcmdvds 11796 divgcdodd 11857 cnptoprest 12447 lmss 12454 txlm 12487 |
Copyright terms: Public domain | W3C validator |