Theorem bianfd

Description: A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995) (Proof shortened by Wolf Lammen, 5-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		bianfd.1	$$⊢\phi \to \neg \psi$$
2	1	intnanrd	$$⊢\phi \to \neg \left(\psi \wedge \chi \right)$$
3	1 2	2falsed	$$⊢\phi \to \left(\psi \leftrightarrow \left(\psi \wedge \chi \right)\right)$$