ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  inegd GIF version

Theorem inegd 1372
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
StepHypRef Expression
1 inegd.1 . . 3 ((𝜑𝜓) → ⊥)
21ex 115 . 2 (𝜑 → (𝜓 → ⊥))
3 dfnot 1371 . 2 𝜓 ↔ (𝜓 → ⊥))
42, 3sylibr 134 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wfal 1358
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 614  ax-in2 615
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359
This theorem is referenced by:  genpdisj  7522  cauappcvgprlemdisj  7650  caucvgprlemdisj  7673  caucvgprprlemdisj  7701  suplocexprlemdisj  7719  suplocexprlemub  7722  suplocsrlem  7807  resqrexlemgt0  11029  resqrexlemoverl  11030  leabs  11083  climge0  11333  isprm5lem  12141  ennnfonelemex  12415  dedekindeu  14104  dedekindicclemicc  14113  pw1nct  14755
  Copyright terms: Public domain W3C validator