Theorem bianbi

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

Hypotheses
bianbi.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
bianbi.2
\( \vdash \psi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \leftrightarrow \theta \wedge \chi \)
Proof
l0
bianbi.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
bianbi.2
anbi1i _
\( \vdash \psi \wedge \chi \leftrightarrow \theta \wedge \chi \)
bitri l0 _