IMP is really NOT( A AND NOT ( B ) )

A → B |- ~(A & ~B)

1) A → B [by assumption] 1

2) A & ~B [by assumption] 2

3) A [conj. elim. 2] 2

4) B [imp by 1,2] 1,2

5) ~B [conj. elim 2] 2

6) B & ~B [conj 4,5] 1,2

7) ~(A & ~B) [reductio ad absurdum 2,6] 1

{Thus by assuming only A → B we prove that we can derive ~(A & ~B).}

From there you can also trivially prove that ~(A & ~B) |- A → B; thus, they are tautologous and so given the primitives ~ and &, implication is not quite as "special" for a Universal Turing machine. This is merely to show, independent of any construction using only IMP, one can trivially reduce it to more primitive components, thus undermining any claim to a "special" status in the context of universal computation.