Theorem syl3anbrc

Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses
syl3anbrc.1
\( \vdash \varphi \rightarrow \psi \)
syl3anbrc.2
\( \vdash \varphi \rightarrow \chi \)
syl3anbrc.3
\( \vdash \varphi \rightarrow \theta \)
syl3anbrc.4
\( \vdash \tau \leftrightarrow \psi \wedge \chi \wedge \theta \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
syl3anbrc.1
l1
syl3anbrc.2
syl3anbrc.3
l3
3jca l0 l1 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
syl3anbrc.4
\( \vdash \tau \leftrightarrow \psi \wedge \chi \wedge \theta \)
sylibr l3 _