Theorem orordir

Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)

Conclusion
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \chi \vee (\psi \vee \chi) \)
Proof
oridm
l1
orbi2i _
\( \vdash \varphi \vee \psi \vee (\chi \vee \chi) \leftrightarrow \varphi \vee \psi \vee \chi \)
or4
\( \vdash \varphi \vee \psi \vee (\chi \vee \chi) \leftrightarrow \varphi \vee \chi \vee (\psi \vee \chi) \)
bitr3i l1 _