Theorem inegd 1414

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

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

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 617  ax-in2 618

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

This theorem is referenced by:  genpdisj  7710  cauappcvgprlemdisj  7838  caucvgprlemdisj  7861  caucvgprprlemdisj  7889  suplocexprlemdisj  7907  suplocexprlemub  7910  suplocsrlem  7995  resqrexlemgt0  11531  resqrexlemoverl  11532  leabs  11585  climge0  11836  isprm5lem  12663  ennnfonelemex  12985  dedekindeu  15297  dedekindicclemicc  15306  pw1nct  16369