Theorem bitr2di

A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses
bitr2di.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bitr2di.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi) \)
Proof
l0
bitr2di.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bitr2di.2
\( \vdash \chi \leftrightarrow \theta \)
bitrdi l0 _
bicomd _