Full Idea
The proof that P∧Q -||- ¬(P → ¬Q) is useful for enabling us to change conjunctions into negated conditionals.
Gist of Idea
We can change conjunctions into negated conditionals with P→Q -||- ¬(P → ¬Q)
Source
E.J. Lemmon (Beginning Logic [1965], 2.2)
Book Reference
Lemmon,E.J.: 'Beginning Logic' [Nelson 1979], p.62