Theorem bitr4id

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

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