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 801) and in particular for decidable propositions (see notnotrdc 813). See also notnotnot 608. (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 601 | 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 588 ax-in2 589 |
This theorem is referenced by: notnotd 604 con3d 605 notnotnot 608 notnoti 619 jcn 626 pm3.24 667 biortn 719 dcn 812 const 822 con1dc 826 notnotbdc 842 imanst 858 eueq2dc 2830 ddifstab 3178 ismkvnex 6997 xrlttri3 9551 nltpnft 9565 ngtmnft 9568 bj-nnsn 12872 bj-nndcALT 12890 bdnthALT 12960 |
Copyright terms: Public domain | W3C validator |