[housecarpenter]

You might be interested to know that in intuitionistic logic, you still have a one-sided contrapositive law, i.e. (A > B) > (~B > ~A):

  [1] A > B(assumption)
  [2] ~B (assumption)
  [3] A (assumption)
  [4] B (modus ponens on 1 and 3)
  [5] ~A (proof of negation on 3, 4 and 2)

It's only the converse that no longer holds. In general familiar equivalences from classical logic are still valid in intuitionistic logic but only in one direction.