Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / d / i / Solution

Put $F=(\neg P)\to Q$ and $G=(\neg P)\to \neg Q$. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule:Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of $F$. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.