Theorem 3syl

Inference chaining two syllogisms syl. Inference associated with imim12i. (Contributed by NM, 28-Dec-1992.)

Hypotheses
3syl.1
\( \vdash \varphi \rightarrow \psi \)
3syl.2
\( \vdash \psi \rightarrow \chi \)
3syl.3
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
3syl.1
\( \vdash \varphi \rightarrow \psi \)
3syl.2
\( \vdash \psi \rightarrow \chi \)
l2
syl l0 _
\( \vdash \varphi \rightarrow \chi \)
3syl.3
\( \vdash \chi \rightarrow \theta \)
syl l2 _