Theorem inegd 1392

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

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

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 1376  df-fal 1379

This theorem is referenced by:  genpdisj  7671  cauappcvgprlemdisj  7799  caucvgprlemdisj  7822  caucvgprprlemdisj  7850  suplocexprlemdisj  7868  suplocexprlemub  7871  suplocsrlem  7956  resqrexlemgt0  11446  resqrexlemoverl  11447  leabs  11500  climge0  11751  isprm5lem  12578  ennnfonelemex  12900  dedekindeu  15210  dedekindicclemicc  15219  pw1nct  16142