Theorem or4

Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)

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