Theorem orordi

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

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