Theorem bitrdi

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

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