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 826) and in particular for decidable propositions (see notnotrdc 838). See also notnotnot 629. (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 622 | 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 609 ax-in2 610 |
This theorem is referenced by: notnotd 625 con3d 626 notnotnot 629 notnoti 640 pm3.24 688 biortn 740 dcn 837 con1dc 851 notnotbdc 867 imanst 883 eueq2dc 2903 ddifstab 3259 ifnotdc 3562 ismkvnex 7131 xrlttri3 9754 nltpnft 9771 ngtmnft 9774 bj-nnsn 13768 bj-nndcALT 13793 bdnthALT 13870 |
Copyright terms: Public domain | W3C validator |