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/iv/solution

Assume under label , under label , and under label . A temporary case assumption gives by the modus ponens rule using . A temporary case assumption gives by the modus ponens rule using . The disjunction elimination rule discharges these case assumptions and concludes under .
Apply the implication introduction rule three times, discharging , then , then . The resulting theorem is
The displayed parentheses make explicit the right association of the source formula.

New to topics? Read the docs here!