Theorem 3bior1fd

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

Hypothesis
3biorfd.1
\( \vdash \varphi \rightarrow \neg \theta \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \vee \psi \leftrightarrow \theta \vee \chi \vee \psi) \)
Proof
l0
3biorfd.1
\( \vdash \varphi \rightarrow \neg \theta \)
biorf
\( \vdash \neg \theta \rightarrow (\chi \vee \psi \leftrightarrow \theta \vee (\chi \vee \psi)) \)
l2
syl l0 _
\( \vdash \varphi \rightarrow (\chi \vee \psi \leftrightarrow \theta \vee (\chi \vee \psi)) \)
3orass
\( \vdash \theta \vee \chi \vee \psi \leftrightarrow \theta \vee (\chi \vee \psi) \)
bitr4di l2 _