Theorem imim1

A closed form of syllogism (see syl ). Theorem *2.06 of [WhiteheadRussell] p. 100. Its associated inference is imim1i. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)

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