Theorem annim

Description: Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	annim	$$⊢\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		iman	$$⊢\left(\phi \to \psi \right)\leftrightarrow \neg \left(\phi \wedge \neg \psi \right)$$
2	1	con2bii	$$⊢\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \left(\phi \to \psi \right)$$