Theorem 3orcoma

Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \psi \vee \varphi \vee \chi \)
Proof
l0
or12
\( \vdash \varphi \vee (\psi \vee \chi) \leftrightarrow \psi \vee (\varphi \vee \chi) \)
l1
3orass
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee (\psi \vee \chi) \)
3orass
\( \vdash \psi \vee \varphi \vee \chi \leftrightarrow \psi \vee (\varphi \vee \chi) \)
3bitr4i l0 l1 _