Theorem 3orrot

Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)

Conclusion
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \psi \vee \chi \vee \varphi \)
Proof
l0
orcom
\( \vdash \varphi \vee (\psi \vee \chi) \leftrightarrow \psi \vee \chi \vee \varphi \)
l1
3orass
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee (\psi \vee \chi) \)
df-3or
\( \vdash \psi \vee \chi \vee \varphi \leftrightarrow \psi \vee \chi \vee \varphi \)
3bitr4i l0 l1 _