Theorem imim3i

Inference adding three nested antecedents. (Contributed by NM, 19-Dec-2006.)

Hypothesis
imim3i.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash (\theta \rightarrow \varphi) \rightarrow (\theta \rightarrow \psi) \rightarrow \theta \rightarrow \chi \)
Proof
imim3i.1
imim2i _
a2d _