Theorem sylanbrc

Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

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