| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > inegd | GIF version | ||
| Description: Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
| Ref | Expression |
|---|---|
| inegd.1 | ⊢ ((𝜑 ∧ 𝜓) → ⊥) |
| Ref | Expression |
|---|---|
| inegd | ⊢ (𝜑 → ¬ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inegd.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ⊥) | |
| 2 | 1 | ex 115 | . 2 ⊢ (𝜑 → (𝜓 → ⊥)) |
| 3 | dfnot 1390 | . 2 ⊢ (¬ 𝜓 ↔ (𝜓 → ⊥)) | |
| 4 | 2, 3 | sylibr 134 | 1 ⊢ (𝜑 → ¬ 𝜓) |
| Colors of variables: wff set class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ⊥wfal 1377 |
| 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 1375 df-fal 1378 |
| This theorem is referenced by: genpdisj 7635 cauappcvgprlemdisj 7763 caucvgprlemdisj 7786 caucvgprprlemdisj 7814 suplocexprlemdisj 7832 suplocexprlemub 7835 suplocsrlem 7920 resqrexlemgt0 11302 resqrexlemoverl 11303 leabs 11356 climge0 11607 isprm5lem 12434 ennnfonelemex 12756 dedekindeu 15066 dedekindicclemicc 15075 pw1nct 15902 |
| Copyright terms: Public domain | W3C validator |