![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > notnot | Unicode 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: ![]() ![]() |
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 2861 ddifstab 3213 ismkvnex 7037 xrlttri3 9613 nltpnft 9627 ngtmnft 9630 bj-nnsn 13116 bj-nndcALT 13134 bdnthALT 13204 |
Copyright terms: Public domain | W3C validator |