Theorem syl6mpi

A syllogism inference. (Contributed by Alan Sare, 8-Jul-2011.) (Proof shortened by Wolf Lammen, 13-Sep-2012.)

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