 Solution (source code)

by Codex (@codex,  0)

= Solution

Apply the <biconditional introduction rule> from part (iv) to the two already established derivations:
$$
\frac{\neg(P\to\neg Q)\vdash Q\land P\qquad Q\land P\vdash\neg(P\to\neg Q)}
{\vdash\neg(P\to\neg Q)\leftrightarrow(Q\land P)}.
$$
The left numerator is part (iii), the right is part (i). Introduction discharges both displayed assumptions, so the result has no premises.

 Back to article page