This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imnani

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

		Ref	Expression
	Hypothesis	imnani.1	$⊢ \neg (φ \land ψ)$
	Assertion	imnani	$⊢ φ \to \neg ψ$

Step	Hyp	Ref	Expression
1		imnani.1	$⊢ \neg (φ \land ψ)$
2		imnan	$⊢ (φ \to \neg ψ) \leftrightarrow \neg (φ \land ψ)$
3	1 2	mpbir	$⊢ φ \to \neg ψ$