Theorem sylancbr

A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)

Hypotheses
sylancbr.1
\( \vdash \psi \leftrightarrow \varphi \)
sylancbr.2
\( \vdash \chi \leftrightarrow \varphi \)
sylancbr.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
sylancbr.1
\( \vdash \psi \leftrightarrow \varphi \)
l1
sylancbr.2
\( \vdash \chi \leftrightarrow \varphi \)
sylancbr.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
syl2anbr l0 l1 _
anidms _