There is a much easier way. See below.

Dan


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

Suppose...

1 ~A => ~B
Premise

2 ~~B => ~~A
Contra, 1

3 B => ~~A
Rem DNeg, 2

4 B => A
Rem DNeg, 3

As Required:

5 ~A => ~B => [B => A]
Conclusion, 1



--- In dcproof@yahoogroups.com, "iquine" <iquine@y...> wrote:
> 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