Theorem orass

Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

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