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

Metamath Proof Explorer

Theorem con2d

Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993)

		Ref	Expression
	Hypothesis	con2d.1	$⊢ φ \to (ψ \to \neg χ)$
	Assertion	con2d	$⊢ φ \to (χ \to \neg ψ)$

Step	Hyp	Ref	Expression
1		con2d.1	$⊢ φ \to (ψ \to \neg χ)$
2		notnotr	$⊢ \neg \neg ψ \to ψ$
3	2 1	syl5	$⊢ φ \to (\neg \neg ψ \to \neg χ)$
4	3	con4d	$⊢ φ \to (χ \to \neg ψ)$