Theorem bitr3id

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

Hypotheses
bitr3id.1
\( \vdash \psi \leftrightarrow \varphi \)
bitr3id.2
\( \vdash \chi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \chi \rightarrow (\varphi \leftrightarrow \theta) \)
Proof
bitr3id.1
l1
bicomi _
\( \vdash \varphi \leftrightarrow \psi \)
bitr3id.2
\( \vdash \chi \rightarrow (\psi \leftrightarrow \theta) \)
bitrid l1 _