Theorem bianfi

Description: A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 26-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		bianfi.1	$$⊢\neg \phi$$
2	1	intnan	$$⊢\neg \left(\psi \wedge \phi \right)$$
3	1 2	2false	$$⊢\phi \leftrightarrow \left(\psi \wedge \phi \right)$$