Theorem imim2

A closed form of syllogism (see syl ). Theorem *2.05 of [WhiteheadRussell] p. 100. Its associated inference is imim2i. Its associated deduction is imim2d. An alternate proof from more basic results is given by [ax-1] followed by a2d. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 6-Sep-2012.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\chi \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
Proof
id
imim2d _