Theorem sylbida

A syllogism deduction. (Contributed by SN, 16-Jul-2024.)

Hypotheses
sylbida.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
sylbida.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
sylbida.1
l1
biimpa _
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
sylbida.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
syldan l1 _