Theorem 3orcomb

Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)

Conclusion
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \chi \vee \psi \)
Proof
l0
3orcoma
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \psi \vee \varphi \vee \chi \)
3orrot
\( \vdash \psi \vee \varphi \vee \chi \leftrightarrow \varphi \vee \chi \vee \psi \)
bitri l0 _