Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 7 / a / i / Solution

Use conjunction elimination to obtain both premises needed for a contradiction under a temporary implication assumption. The following natural deduction derivation discharges precisely assumption 4:Here $\to E$ is the implication elimination rule and $\neg I$ is negation introduction. The original conjunction remains the only undischarged premise.