Theorem birot

Rotation of the arguments of the nested implication ( . <-> ( . <-> . ) ) (a general phenomenon for a commutative associative binary operation, see e.g., [inrot]) . (Contributed by BJ, 10-Aug-2026.)

Conclusion
\( \vdash \varphi \leftrightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\psi \leftrightarrow (\chi \leftrightarrow \varphi)) \)
Proof
l0
bicom
\( \vdash \varphi \leftrightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\psi \leftrightarrow \chi \leftrightarrow \varphi) \)
biass
\( \vdash \psi \leftrightarrow \chi \leftrightarrow \varphi \leftrightarrow (\psi \leftrightarrow (\chi \leftrightarrow \varphi)) \)
bitri l0 _