Theorem biorfd

Description: A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023)

	Ref	Expression
Hypothesis	biorfd.1	$$⊢\phi \to \neg \psi$$
Assertion	biorfd	$$⊢\phi \to \left(\chi \leftrightarrow \left(\psi \vee \chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		biorfd.1	$$⊢\phi \to \neg \psi$$
2		biorf	$$⊢\neg \psi \to \left(\chi \leftrightarrow \left(\psi \vee \chi \right)\right)$$
3	1 2	syl	$$⊢\phi \to \left(\chi \leftrightarrow \left(\psi \vee \chi \right)\right)$$