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

Assume $E\to G$ under label $a$, $F\to G$ under label $b$, and $E\vee F$ under label $c$. A temporary case assumption $E$ gives $G$ by the modus ponens rule using $a$. A temporary case assumption $F$ gives $G$ by the modus ponens rule using $b$. The disjunction elimination rule discharges these case assumptions and concludes $G$ under $a,b,c$.

Apply the implication introduction rule three times, discharging $c$, then $b$, then $a$. The resulting theorem isThe displayed parentheses make explicit the right association of the source formula.