Theorem 3bior2fd

A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf. (Contributed by Alexander van der Vekens, 8-Sep-2017.)

Hypotheses
3biorfd.1
\( \vdash \varphi \rightarrow \neg \theta \)
3biorfd.2
\( \vdash \varphi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta \vee \chi \vee \psi) \)
Proof
l0
3biorfd.2
\( \vdash \varphi \rightarrow \neg \chi \)
biorf
\( \vdash \neg \chi \rightarrow (\psi \leftrightarrow \chi \vee \psi) \)
l2
syl l0 _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \vee \psi) \)
3biorfd.1
3bior1fd _
\( \vdash \varphi \rightarrow (\chi \vee \psi \leftrightarrow \theta \vee \chi \vee \psi) \)
bitrd l2 _