Theorem sylancb

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

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