Theorem bitr4di

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

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