Theorem bitr3di

A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

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