Theorem 3bior1fand

A disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction. (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 \wedge \tau \vee \chi \vee \psi) \)
Proof
3biorfd.1
intnanrd _
3bior1fd _