Theorem inegd 1417

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

Hypothesis

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

Assertion

Ref	Expression
inegd	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem inegd

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104  ⊥wfal 1403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404

This theorem is referenced by:  genpdisj  7838  cauappcvgprlemdisj  7966  caucvgprlemdisj  7989  caucvgprprlemdisj  8017  suplocexprlemdisj  8035  suplocexprlemub  8038  suplocsrlem  8123  resqrexlemgt0  11705  resqrexlemoverl  11706  leabs  11759  climge0  12010  isprm5lem  12838  ennnfonelemex  13165  dedekindeu  15488  dedekindicclemicc  15497  usgr1vr  16243  pw1nct  16777