Theorem or42

Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)

Conclusion
\( \vdash \varphi \vee \psi \vee (\chi \vee \theta) \leftrightarrow \varphi \vee \chi \vee (\theta \vee \psi) \)
Proof
l0
or4
\( \vdash \varphi \vee \psi \vee (\chi \vee \theta) \leftrightarrow \varphi \vee \chi \vee (\psi \vee \theta) \)
orcom
orbi2i _
\( \vdash \varphi \vee \chi \vee (\psi \vee \theta) \leftrightarrow \varphi \vee \chi \vee (\theta \vee \psi) \)
bitri l0 _