Theorem syl21anbrc

Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)

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