Theorem inegd 1367

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103  ⊥wfal 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354

This theorem is referenced by:  genpdisj  7472  cauappcvgprlemdisj  7600  caucvgprlemdisj  7623  caucvgprprlemdisj  7651  suplocexprlemdisj  7669  suplocexprlemub  7672  suplocsrlem  7757  resqrexlemgt0  10971  resqrexlemoverl  10972  leabs  11025  climge0  11275  isprm5lem  12082  ennnfonelemex  12356  dedekindeu  13354  dedekindicclemicc  13363  pw1nct  13996