Theorem syl3anb

A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)

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