Theorem 4syl

Inference chaining three syllogisms syl. (Contributed by BJ, 14-Jul-2018.) The use of this theorem is marked "discouraged" because it can cause the Metamath program "MM-PA> MINIMIZE__WITH *" command to have very long run times. However, feel free to use "MM-PA> MINIMIZE__WITH 4syl / OVERRIDE" if you wish. Remember to update the "discouraged" file if it gets used. (New usage is discouraged.)

Hypotheses
4syl.1
\( \vdash \varphi \rightarrow \psi \)
4syl.2
\( \vdash \psi \rightarrow \chi \)
4syl.3
\( \vdash \chi \rightarrow \theta \)
4syl.4
\( \vdash \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
4syl.1
\( \vdash \varphi \rightarrow \psi \)
l1
4syl.2
\( \vdash \psi \rightarrow \chi \)
4syl.3
\( \vdash \chi \rightarrow \theta \)
l3
3syl l0 l1 _
\( \vdash \varphi \rightarrow \theta \)
4syl.4
\( \vdash \theta \rightarrow \tau \)
syl l3 _