Theorem biorfi

Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 16-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		biorfi.1	$$⊢\neg \phi$$
2		orc	$$⊢\psi \to \left(\psi \vee \phi \right)$$
3		pm2.53	$$⊢\left(\psi \vee \phi \right)\to \left(\neg \psi \to \phi \right)$$
4	1 3	mt3i	$$⊢\left(\psi \vee \phi \right)\to \psi$$
5	2 4	impbii	$$⊢\psi \leftrightarrow \left(\psi \vee \phi \right)$$