Example 5

We will prove:

A
~B
~(A B)

Our conclusion is the negation of a biconditional of A, B. Our premises are A, and ~B. We don't have the biconditional or its negation in any premises. Our only hope will be to reach the conclusion using Biconditional Exchange "inside" the negation. Thinking backward will lead us to the following six steps:

 

~~A & ~B
(~~A & ~B) v ~(B A)
~(~A v B) v ~(B A)
~[(~A v B) & (B A)]
~[(A B) & (B A)]
~(A B)
 

Before looking at the proof, you should make sure how we reached this sequence, starting from the last wff and working up.  Then it should be a piece of cake to construct the proof:

line number wff justification line number
1. A    
2. ~B    
3. ~~A D.N. 1
4. ~~A & ~B conj. 2,3
5. (~~A & ~B) v ~(B A) disj. 4
6. ~(~A v B) v ~(B A) Dem 5
7. ~[(~A v B) & (B A)] Dem 6
8. ~[(A B) & (B A)] C.E. 7
9. ~(A B) B.E 8