Theorem sylan9bbr

Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses
sylan9bbr.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
sylan9bbr.2
\( \vdash \theta \rightarrow (\chi \leftrightarrow \tau) \)
Conclusion
\( \vdash \theta \wedge \varphi \rightarrow (\psi \leftrightarrow \tau) \)
Proof
l0
sylan9bbr.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
sylan9bbr.2
\( \vdash \theta \rightarrow (\chi \leftrightarrow \tau) \)
sylan9bb l0 _
ancoms _