Theorem con3d

Description: A contraposition deduction. Deduction form of con3 . (Contributed by NM, 10-Jan-1993)

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

Proof

Step	Hyp	Ref	Expression
1		con3d.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		notnotr	$$⊢\neg \neg \psi \to \psi$$
3	2 1	syl5	$$⊢\phi \to \left(\neg \neg \psi \to \chi \right)$$
4	3	con1d	$$⊢\phi \to \left(\neg \chi \to \neg \psi \right)$$