Theorem 3orbi123i

Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)

Hypotheses
bi3.1
\( \vdash \varphi \leftrightarrow \psi \)
bi3.2
\( \vdash \chi \leftrightarrow \theta \)
bi3.3
\( \vdash \tau \leftrightarrow \eta \)
Conclusion
\( \vdash \varphi \vee \chi \vee \tau \leftrightarrow \psi \vee \theta \vee \eta \)
Proof
l0
bi3.1
bi3.2
l2
orbi12i l0 _
bi3.3
l4
orbi12i l2 _
\( \vdash \varphi \vee \chi \vee \tau \leftrightarrow \psi \vee \theta \vee \eta \)
l5
df-3or
\( \vdash \varphi \vee \chi \vee \tau \leftrightarrow \varphi \vee \chi \vee \tau \)
df-3or
\( \vdash \psi \vee \theta \vee \eta \leftrightarrow \psi \vee \theta \vee \eta \)
3bitr4i l4 l5 _