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

Metamath Proof Explorer

Theorem pm2.01da

Description: Deduction based on reductio ad absurdum. See pm2.01 . (Contributed by Mario Carneiro, 9-Feb-2017)

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

Step	Hyp	Ref	Expression
1		pm2.01da.1	$⊢ (φ \land ψ) \to \neg ψ$
2	1	ex	$⊢ φ \to (ψ \to \neg ψ)$
3	2	pm2.01d	$⊢ φ \to \neg ψ$