Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/digital-systems-linear-algebra-introduction-to-formal-proof/7/a/ii/solution

Keep the four given premises in context and assume under label . The modus ponens rule applied to the first two premises gives and . Apply the disjunction elimination rule to as follows.
Under a case assumption , the premise gives by the modus ponens rule. Together with , the negation elimination rule gives , and the supplied logical falsity elimination rule gives . Under the other case assumption , the required conclusion is already available. Discharge both case assumptions with the disjunction elimination rule to conclude .
Finally discharge with the implication introduction rule, giving . The premise is not needed: a derivation is permitted to leave a premise unused.

New to topics? Read the docs here!