Theorem sylanblc

Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)

Hypotheses
sylanblc.1
\( \vdash \varphi \rightarrow \psi \)
sylanblc.2
\( \vdash \chi \)
sylanblc.3
\( \vdash \psi \wedge \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
sylanblc.1
\( \vdash \varphi \rightarrow \psi \)
l1
sylanblc.2
\( \vdash \chi \)
sylanblc.3
biimpi _
\( \vdash \psi \wedge \chi \rightarrow \theta \)
sylancl l0 l1 _