Theorem contrd

Description: A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)

	Ref	Expression
Hypotheses	contrd.1	$$⊢\phi \to \left(\neg \psi \to \chi \right)$$
	contrd.2	$$⊢\phi \to \left(\neg \psi \to \neg \chi \right)$$
Assertion	contrd	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		contrd.1	$$⊢\phi \to \left(\neg \psi \to \chi \right)$$
2		contrd.2	$$⊢\phi \to \left(\neg \psi \to \neg \chi \right)$$
3	1 2	jcad	$$⊢\phi \to \left(\neg \psi \to \left(\chi \wedge \neg \chi \right)\right)$$
4		pm2.24	$$⊢\chi \to \left(\neg \chi \to \psi \right)$$
5	4	imp	$$⊢\left(\chi \wedge \neg \chi \right)\to \psi$$
6	5	imim2i	$$⊢\left(\neg \psi \to \left(\chi \wedge \neg \chi \right)\right)\to \left(\neg \psi \to \psi \right)$$
7	6	pm2.18d	$$⊢\left(\neg \psi \to \left(\chi \wedge \neg \chi \right)\right)\to \psi$$
8	3 7	syl	$$⊢\phi \to \psi$$