[superobserver]

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.

[kmill]

Rather than deducing it, you can also look at the truth table, see it is 0 exactly where B is not true and A is true, and get not(A and not B). Then, we can conclude there is a proof such as yours from the completeness theorem, I believe.

[superobserver]

Yes, but it's more fun and edifying to prove it. :) It's so rare I get an opportunity to whip out propositional logic and formal proof methods that I hardly balk at the opportunity. (hears groans from non-nerds)

[Breakthrough]

If you use DeMorgan's law on your result, you can simplify it further to ~A | B