Theorem syl3an9b

Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)

Hypotheses
syl3an9b.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
syl3an9b.2
\( \vdash \theta \rightarrow (\chi \leftrightarrow \tau) \)
syl3an9b.3
\( \vdash \eta \rightarrow (\tau \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \wedge \theta \wedge \eta \rightarrow (\psi \leftrightarrow \zeta) \)
Proof
l0
syl3an9b.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
syl3an9b.2
\( \vdash \theta \rightarrow (\chi \leftrightarrow \tau) \)
l2
sylan9bb l0 _
\( \vdash \varphi \wedge \theta \rightarrow (\psi \leftrightarrow \tau) \)
syl3an9b.3
\( \vdash \eta \rightarrow (\tau \leftrightarrow \zeta) \)
sylan9bb l2 _
3impa _