Closed form of al2imi. Version of alim for a nested implication.
(Contributed by Alan Sare, 31-Dec-2011.)
\( \vdash \forall x \, (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, \psi \rightarrow \forall x \, \chi \)
\( \vdash \forall x \, (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, (\psi \rightarrow \chi) \)
\( \vdash \forall x \, (\psi \rightarrow \chi) \rightarrow \forall x \, \psi \rightarrow \forall x \, \chi \)