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  7891  cauappcvgprlemdisj  8019  caucvgprlemdisj  8042  caucvgprprlemdisj  8070  suplocexprlemdisj  8088  suplocexprlemub  8091  suplocsrlem  8176  resqrexlemgt0  11802  resqrexlemoverl  11803  leabs  11856  climge0  12110  isprm5lem  12939  ennnfonelemex  13357  dedekindeu  15815  dedekindicclemicc  15824  usgr1vr  16655  pw1nct  17199