= Solution
Use <conjunction elimination> to extract the three inputs, then apply the <implication elimination rule> three times:
$$
\begin{array}{rll}
1&E\to(F\to(G\to H))&\text{premise}\\
2&\vert\ (E\land F)\land G&\text{assumption}\\
3&\vert\ E\land F&\land\text{-elim-L }2\\
4&\vert\ G&\land\text{-elim-R }2\\
5&\vert\ E&\land\text{-elim-L }3\\
6&\vert\ F&\land\text{-elim-R }3\\
7&\vert\ F\to(G\to H)&\to\text{-elim }1,5\\
8&\vert\ G\to H&\to\text{-elim }7,6\\
9&\vert\ H&\to\text{-elim }8,4\\
10&((E\land F)\land G)\to H&\to\text{-intro }2\text{--}9
\end{array}
$$
The <implication introduction rule> closes the only <subproof>, giving
$$
\boxed{E\to F\to G\to H\ \vdash\ ((E\land F)\land G)\to H.}
$$
Back to article page
