Theorem sylanblrc

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

Hypotheses
sylanblrc.1
\( \vdash \varphi \rightarrow \psi \)
sylanblrc.2
\( \vdash \chi \)
sylanblrc.3
\( \vdash \theta \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
sylanblrc.1
\( \vdash \varphi \rightarrow \psi \)
sylanblrc.2
l2
a1i _
\( \vdash \varphi \rightarrow \chi \)
sylanblrc.3
\( \vdash \theta \leftrightarrow \psi \wedge \chi \)
sylanbrc l0 l2 _