THEOREM

*******

[A => B] <=> ~[A & ~B]

PROOF

*****

'=>'

Suppose...

1     A => B

Premise

Suppose to the contrary...

2     A & ~B

Premise

3     A

Split, 2

4     ~B

Split, 2

Apply Detachment Rule

5     B

Detach, 1, 3

Obtain the contradiction...

6     B & ~B

Join, 5, 4

Apply Conclusion Rule (By Contradiction)

7     ~[A & ~B]

4 Conclusion, 2

'=>'

Apply Conclusion Rule (Direct Proof)

8     A => B => ~[A & ~B]

4 Conclusion, 1

'<='

Suppose...

9     ~[A & ~B]

Premise

Suppose...

10   A

Premise

Suppose to the contrary...

11   ~B

Premise

12   A & ~B

Join, 10, 11

Obtain the contradiction...

13   A & ~B & ~[A & ~B]

Join, 12, 9

Apply Conclusion Rule (By Contradiction)

14   ~~B

4 Conclusion, 11

15   B

Rem DNeg, 14

Apply Conclusion Rule (Direct Proof)

16   A => B

4 Conclusion, 10

'<='

Apply Conclusion Rule (Direct Proof)

17   ~[A & ~B] => [A => B]

4 Conclusion, 9

18   [A => B => ~[A & ~B]] & [~[A & ~B] => [A => B]]

Join, 8, 17

As Required:

19   A => B <=> ~[A & ~B]

Iff-And, 18