Theorem con3dimp

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

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

Proof

Step	Hyp	Ref	Expression
1		con3dimp.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2	1	con3d	$$⊢\phi \to \left(\neg \chi \to \neg \psi \right)$$
3	2	imp	$$⊢\left(\phi \wedge \neg \chi \right)\to \neg \psi$$