![]() |
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 831) and in particular for decidable propositions (see notnotrdc 843). See also notnotnot 634. (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 627 |
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 614 ax-in2 615 |
This theorem is referenced by: notnotd 630 con3d 631 notnotnot 634 notnoti 645 pm3.24 693 biortn 745 dcn 842 con1dc 856 notnotbdc 872 imanst 888 eueq2dc 2910 ddifstab 3267 ifnotdc 3570 ismkvnex 7147 xrlttri3 9781 nltpnft 9798 ngtmnft 9801 bj-nnsn 14134 bj-nndcALT 14159 bdnthALT 14236 |
Copyright terms: Public domain | W3C validator |