Theorem sylan2b

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

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