Theorem syl3anbr

A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)

Hypotheses
syl3anbr.1
\( \vdash \psi \leftrightarrow \varphi \)
syl3anbr.2
\( \vdash \theta \leftrightarrow \chi \)
syl3anbr.3
\( \vdash \eta \leftrightarrow \tau \)
syl3anbr.4
\( \vdash \psi \wedge \theta \wedge \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \tau \rightarrow \zeta \)
Proof
syl3anbr.1
l1
bicomi _
\( \vdash \varphi \leftrightarrow \psi \)
syl3anbr.2
l3
bicomi _
\( \vdash \chi \leftrightarrow \theta \)
syl3anbr.3
l5
bicomi _
\( \vdash \tau \leftrightarrow \eta \)
syl3anbr.4
\( \vdash \psi \wedge \theta \wedge \eta \rightarrow \zeta \)
syl3anb l1 l3 l5 _