Theorem 13an22anass
Associative law for four conjunctions with a triple conjunction.
(Contributed by Thierry Arnoux, 21-Jan-2025.)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \theta) \)
Proof
l0
an2anr
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \varphi) \leftrightarrow \chi \wedge \psi \wedge (\varphi \wedge \theta) \)
l1
an2anr
\( \vdash \varphi \wedge \chi \wedge (\theta \wedge \psi) \leftrightarrow \chi \wedge \varphi \wedge (\psi \wedge \theta) \)
an4
\( \vdash \chi \wedge \varphi \wedge (\psi \wedge \theta) \leftrightarrow \chi \wedge \psi \wedge (\varphi \wedge \theta) \)
l3
bitri l1 _
\( \vdash \varphi \wedge \chi \wedge (\theta \wedge \psi) \leftrightarrow \chi \wedge \psi \wedge (\varphi \wedge \theta) \)
an43
\( \vdash \varphi \wedge \chi \wedge (\theta \wedge \psi) \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \theta) \)
l5
3bitr2ri l0 l3 _
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge \varphi) \)
l6
3an4anass
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge \varphi \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge \varphi) \)
ancom
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge \varphi \leftrightarrow \varphi \wedge (\psi \wedge \chi \wedge \theta) \)
3bitr2ri l5 l6 _