Theorem bitrid

A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

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