Theorem syl8ib

A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.)

Hypotheses
syl8ib.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
syl8ib.2
\( \vdash \theta \leftrightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \)
Proof
l0
syl8ib.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
syl8ib.2
biimpi _
\( \vdash \theta \rightarrow \tau \)
syl8 l0 _