Theorem con3d

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

	Ref	Expression
Hypothesis	con3d.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	con3d	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		con3d.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		notnotr	⊢ ( ¬ ¬ 𝜓 → 𝜓 )
3	2 1	syl5	⊢ ( 𝜑 → ( ¬ ¬ 𝜓 → 𝜒 ) )
4	3	con1d	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) )