Theorem contrd

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

	Ref	Expression
Hypotheses	contrd.1	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
	contrd.2	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜒 ) )
Assertion	contrd	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		contrd.1	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
2		contrd.2	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜒 ) )
3	1 2	jcad	⊢ ( 𝜑 → ( ¬ 𝜓 → ( 𝜒 ∧ ¬ 𝜒 ) ) )
4		pm2.24	⊢ ( 𝜒 → ( ¬ 𝜒 → 𝜓 ) )
5	4	imp	⊢ ( ( 𝜒 ∧ ¬ 𝜒 ) → 𝜓 )
6	5	imim2i	⊢ ( ( ¬ 𝜓 → ( 𝜒 ∧ ¬ 𝜒 ) ) → ( ¬ 𝜓 → 𝜓 ) )
7	6	pm2.18d	⊢ ( ( ¬ 𝜓 → ( 𝜒 ∧ ¬ 𝜒 ) ) → 𝜓 )
8	3 7	syl	⊢ ( 𝜑 → 𝜓 )