Theorem sylan9bb

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

Hypotheses
sylan9bb.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
sylan9bb.2
\( \vdash \theta \rightarrow (\chi \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow (\psi \leftrightarrow \tau) \)
Proof
sylan9bb.1
l1
adantr _
\( \vdash \varphi \wedge \theta \rightarrow (\psi \leftrightarrow \chi) \)
sylan9bb.2
adantl _
\( \vdash \varphi \wedge \theta \rightarrow (\chi \leftrightarrow \tau) \)
bitrd l1 _