Theorem inegd 1383

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

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

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 1367  df-fal 1370

This theorem is referenced by:  genpdisj  7609  cauappcvgprlemdisj  7737  caucvgprlemdisj  7760  caucvgprprlemdisj  7788  suplocexprlemdisj  7806  suplocexprlemub  7809  suplocsrlem  7894  resqrexlemgt0  11204  resqrexlemoverl  11205  leabs  11258  climge0  11509  isprm5lem  12336  ennnfonelemex  12658  dedekindeu  14967  dedekindicclemicc  14976  pw1nct  15758