Theorem inegd 1391

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 1390	. 2 ⊢ (¬ 𝜓 ↔ (𝜓 → ⊥))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-fal 1378

This theorem is referenced by:  genpdisj  7635  cauappcvgprlemdisj  7763  caucvgprlemdisj  7786  caucvgprprlemdisj  7814  suplocexprlemdisj  7832  suplocexprlemub  7835  suplocsrlem  7920  resqrexlemgt0  11302  resqrexlemoverl  11303  leabs  11356  climge0  11607  isprm5lem  12434  ennnfonelemex  12756  dedekindeu  15066  dedekindicclemicc  15075  pw1nct  15902