Theorem syl56

Combine syl5 and syl6. (Contributed by NM, 14-Nov-2013.)

Hypotheses
syl56.1
\( \vdash \varphi \rightarrow \psi \)
syl56.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
syl56.3
\( \vdash \theta \rightarrow \tau \)
Conclusion
\( \vdash \chi \rightarrow \varphi \rightarrow \tau \)
Proof
l0
syl56.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl56.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
syl56.3
\( \vdash \theta \rightarrow \tau \)
syl6 l1 _
\( \vdash \chi \rightarrow \psi \rightarrow \tau \)
syl5 l0 _