Theorem bianim

Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.)

Hypotheses
bianim.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
bianim.2
\( \vdash \chi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \leftrightarrow \theta \wedge \chi \)
Proof
l0
bianim.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
bianim.2
pm5.32ri _
\( \vdash \psi \wedge \chi \leftrightarrow \theta \wedge \chi \)
bitri l0 _