Theorem bitr2id

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

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