Theorem inegd

Description: Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017)

	Ref	Expression
Hypothesis	inegd.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⊥ )
Assertion	inegd	⊢ ( 𝜑 → ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		inegd.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⊥ )
2	1	ex	⊢ ( 𝜑 → ( 𝜓 → ⊥ ) )
3		dfnot	⊢ ( ¬ 𝜓 ↔ ( 𝜓 → ⊥ ) )
4	2 3	sylibr	⊢ ( 𝜑 → ¬ 𝜓 )