Theorem con3dimp

Description: Variant of con3d with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		con3dimp.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2	1	con3d	⊢ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) )
3	2	imp	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ 𝜓 )