Theorem biortn

Description: A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012)

	Ref	Expression
Assertion	biortn	⊢ ( 𝜑 → ( 𝜓 ↔ ( ¬ 𝜑 ∨ 𝜓 ) ) )

Proof

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