Theorem inegd 1421

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104  ⊥wfal 1407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408

This theorem is used by:  genpdisj  7890  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  suplocexprlemdisj  8087  suplocexprlemub  8090  suplocsrlem  8175  resqrexlemgt0  11800  resqrexlemoverl  11801  leabs  11854  climge0  12107  isprm5lem  12936  ennnfonelemex  13354  dedekindeu  15773  dedekindicclemicc  15782  usgr1vr  16587  pw1nct  17131