Theorem iman

Description: Implication in terms of conjunction and negation. Theorem 3.4(27) of Stoll p. 176. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 30-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	$$⊢\psi \leftrightarrow \neg \neg \psi$$
2	1	imbi2i	$$⊢\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \neg \neg \psi \right)$$
3		imnan	$$⊢\left(\phi \to \neg \neg \psi \right)\leftrightarrow \neg \left(\phi \wedge \neg \psi \right)$$
4	2 3	bitri	$$⊢\left(\phi \to \psi \right)\leftrightarrow \neg \left(\phi \wedge \neg \psi \right)$$