Theorem imnani

Description: Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		imnani.1	$$⊢\neg \left(\phi \wedge \psi \right)$$
2		imnan	$$⊢\left(\phi \to \neg \psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$
3	1 2	mpbir	$$⊢\phi \to \neg \psi$$