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	⊢ ( 𝜑 → ¬ 𝜓 )
Assertion	biorfd	⊢ ( 𝜑 → ( 𝜒 ↔ ( 𝜓 ∨ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		biorfd.1	⊢ ( 𝜑 → ¬ 𝜓 )
2		biorf	⊢ ( ¬ 𝜓 → ( 𝜒 ↔ ( 𝜓 ∨ 𝜒 ) ) )
3	1 2	syl	⊢ ( 𝜑 → ( 𝜒 ↔ ( 𝜓 ∨ 𝜒 ) ) )