Theorem biass
Associative law for the biconditional. An axiom of system DS in Vladimir
Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic,
113:207-224, 2002,
http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805.
Interestingly, this law was not included in Principia Mathematica but
was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by
NM, 8-Jan-2005.) (Proof shortened by Juha Arpiainen, 19-Jan-2006.)
(Proof shortened by Wolf Lammen, 21-Sep-2013.)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi)) \)
Proof
pm5.501
l1
bibi1d _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi)) \)
pm5.501
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi))) \)
l3
bitr3d l1 _
\( \vdash \varphi \rightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi))) \)
l4
nbbn
\( \vdash \neg \psi \leftrightarrow \chi \leftrightarrow \neg (\psi \leftrightarrow \chi) \)
nbn2
bibi1d _
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi)) \)
l7
bitr3id l4 _
\( \vdash \neg \varphi \rightarrow (\neg (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi)) \)
nbn2
\( \vdash \neg \varphi \rightarrow (\neg (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi))) \)
bitr3d l7 _
\( \vdash \neg \varphi \rightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi))) \)
pm2.61i l3 _