Theorem or32

A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

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