Dan,

Thanks for the response to my wishlist, will respond to that over the
weekend.

Haven't quite gotten the hang of DCProof yet, and am stuck on a proof
that could easily be done on paper, but can't see how to do it here.

The thereom is an implication, which could easily be proved by
contradiction.

My attempted approach was to prove that the consequent was true if A
was true, and that it also was true if ~A was true, and that therefore
it must be true.

The problem is that, when I try to apply CASES, DCProof allows me to
click on the OR statement in 10 - but it won't allow me to click on
the AND statement in 11, probably because the consequent is not a
single statement letter, but rather an implication in itself.

How would you complete the proof along these same lines?


Prove: (~A=>~B)=>(B=>A)

1 ~A => ~B
Premise

2 ~A
Premise

3 ~B
Detach, 1, 2

4 ~~B => A
Arb Cons, 3

5 B => A
Rem DNeg, 4

6 ~A => [B => A]
Conclusion, 2

7 A
Premise

8 B => A
Arb Ante, 7

9 A => [B => A]
Conclusion, 7

10 ~A | A
Premise

11 [~A => [B => A]] & [A => [B => A]]
Join, 6, 9