Theorem sylan2br

A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses
sylan2br.1
\( \vdash \chi \leftrightarrow \varphi \)
sylan2br.2
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \theta \)
Proof
sylan2br.1
l1
biimpri _
\( \vdash \varphi \rightarrow \chi \)
sylan2br.2
\( \vdash \psi \wedge \chi \rightarrow \theta \)
sylan2 l1 _