Theorem pm2.65i

Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994) (Proof shortened by Wolf Lammen, 11-Sep-2013)

	Ref	Expression
Hypotheses	pm2.65i.1	⊢ ( 𝜑 → 𝜓 )
	pm2.65i.2	⊢ ( 𝜑 → ¬ 𝜓 )
Assertion	pm2.65i	⊢ ¬ 𝜑

Proof

Step	Hyp	Ref	Expression
1		pm2.65i.1	⊢ ( 𝜑 → 𝜓 )
2		pm2.65i.2	⊢ ( 𝜑 → ¬ 𝜓 )
3	2	con2i	⊢ ( 𝜓 → ¬ 𝜑 )
4	1	con3i	⊢ ( ¬ 𝜓 → ¬ 𝜑 )
5	3 4	pm2.61i	⊢ ¬ 𝜑