Theorem 3orass

Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)

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