 Solution

ID: 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/7/b/ii/solution

Use conjunction elimination to extract the three inputs, then apply the implication elimination rule three times:

12345678910 E \to (F \to (G \to H)) ∣ (E \land F) \land G ∣ E \land F ∣ G ∣ E ∣ F ∣ F \to (G \to H) ∣ G \to H ∣ H ((E \land F) \land G) \to H premise assumption \land -elim-L 2 \land -elim-R 2 \land -elim-L 3 \land -elim-R 3 \to -elim 1, 5 \to -elim 7, 6 \to -elim 8, 4 \to -intro 2 - 9

E \to F \to G \to H ⊢ ((E \land F) \land G) \to H .

 New to topics? Read the docs here!