= Solution
Read chained <logical implications> as right-associative. Use the following <natural deduction> derivation; indentation bars mark nested <subproofs> and the last column records rules and discharged line ranges:
$$
\begin{array}{rll}
1&E\to(F\to(G\to H))&\text{premise}\\
2&\vert\ G&\text{assumption}\\
3&\vert\ \vert\ F&\text{assumption}\\
4&\vert\ \vert\ \vert\ E&\text{assumption}\\
5&\vert\ \vert\ \vert\ F\to(G\to H)&\to\text{-elim }1,4\\
6&\vert\ \vert\ \vert\ G\to H&\to\text{-elim }5,3\\
7&\vert\ \vert\ \vert\ H&\to\text{-elim }6,2\\
8&\vert\ \vert\ E\to H&\to\text{-intro }4\text{--}7\\
9&\vert\ F\to(E\to H)&\to\text{-intro }3\text{--}8\\
10&G\to(F\to(E\to H))&\to\text{-intro }2\text{--}9
\end{array}
$$
Each application of the <implication introduction rule> discharges only its matching <temporary assumption>. Thus
$$
\boxed{E\to F\to G\to H\ \vdash\ G\to F\to E\to H.}
$$
Back to article page
