Theorem 3or6

Analogue of or4 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)

Conclusion
\( \vdash (\varphi \vee \psi) \vee (\chi \vee \theta) \vee (\tau \vee \eta) \leftrightarrow \varphi \vee \chi \vee \tau \vee (\psi \vee \theta \vee \eta) \)
Proof
l0
or4
\( \vdash \varphi \vee \chi \vee \tau \vee (\psi \vee \theta \vee \eta) \leftrightarrow \varphi \vee \chi \vee (\psi \vee \theta) \vee (\tau \vee \eta) \)
or4
orbi1i _
\( \vdash \varphi \vee \chi \vee (\psi \vee \theta) \vee (\tau \vee \eta) \leftrightarrow \varphi \vee \psi \vee (\chi \vee \theta) \vee (\tau \vee \eta) \)
l3
bitr2i l0 _
\( \vdash \varphi \vee \psi \vee (\chi \vee \theta) \vee (\tau \vee \eta) \leftrightarrow \varphi \vee \chi \vee \tau \vee (\psi \vee \theta \vee \eta) \)
l4
df-3or
\( \vdash (\varphi \vee \psi) \vee (\chi \vee \theta) \vee (\tau \vee \eta) \leftrightarrow \varphi \vee \psi \vee (\chi \vee \theta) \vee (\tau \vee \eta) \)
l5
df-3or
df-3or
orbi12i l5 _
\( \vdash \varphi \vee \chi \vee \tau \vee (\psi \vee \theta \vee \eta) \leftrightarrow \varphi \vee \chi \vee \tau \vee (\psi \vee \theta \vee \eta) \)
3bitr4i l3 l4 _