![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > notnot1 | Unicode version |
Description: Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
Ref | Expression |
---|---|
notnot1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 | |
2 | 1 | con2i 120 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4 |
This theorem is referenced by: notnoti 123 con1d 124 con4i 130 notnot 291 biortn 406 pm2.13 418 necon2ad 2670 necon4ad 2677 necon4ai 2695 eueq2 3273 ifnot 3986 nbusgra 24428 wlkntrl 24564 eupath2 24980 cnfn1dd 30492 cnfn2dd 30493 stoweidlem39 31821 vk15.4j 33298 zfregs2VD 33641 vk15.4jVD 33714 con3ALTVD 33716 axfrege41 37871 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
Copyright terms: Public domain | W3C validator |