Theorem ninba

Description: Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994)

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

Proof

Step	Hyp	Ref	Expression
1		ninba.1	$$⊢\phi$$
2	1	niabn	$$⊢\neg \psi \to \left(\left(\chi \wedge \psi \right)\leftrightarrow \neg \phi \right)$$
3	2	bicomd	$$⊢\neg \psi \to \left(\neg \phi \leftrightarrow \left(\chi \wedge \psi \right)\right)$$