Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > notnot | GIF version |
Description: Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. The converse need not hold. It holds exactly for stable propositions (by definition, see df-stab 817) and in particular for decidable propositions (see notnotrdc 829). See also notnotnot 624. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
Ref | Expression |
---|---|
notnot | ⊢ (𝜑 → ¬ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (¬ 𝜑 → ¬ 𝜑) | |
2 | 1 | con2i 617 | 1 ⊢ (𝜑 → ¬ ¬ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 604 ax-in2 605 |
This theorem is referenced by: notnotd 620 con3d 621 notnotnot 624 notnoti 635 pm3.24 683 biortn 735 dcn 828 const 838 con1dc 842 notnotbdc 858 imanst 874 eueq2dc 2885 ddifstab 3239 ismkvnex 7098 xrlttri3 9704 nltpnft 9718 ngtmnft 9721 bj-nnsn 13320 bj-nndcALT 13341 bdnthALT 13421 |
Copyright terms: Public domain | W3C validator |