Theorem biluk

Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\chi \leftrightarrow \psi \leftrightarrow (\varphi \leftrightarrow \chi)) \)
Proof
bicom
l1
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow \varphi \leftrightarrow \chi) \)
biass
\( \vdash \psi \leftrightarrow \varphi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi)) \)
l3
bitri l1 _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi)) \)
biass
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi)) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow (\chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi)))) \)
l5
mpbi l3 _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi))) \)
biass
\( \vdash \chi \leftrightarrow \psi \leftrightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\chi \leftrightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \chi))) \)
bitr4i l5 _