![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > notnotr | Structured version Visualization version GIF version |
Description: Double negation elimination. Converse of notnot 142 and one implication of notnotb 314. Theorem *2.14 of [WhiteheadRussell] p. 102. This was the fifth axiom of Frege, specifically Proposition 31 of [Frege1879] p. 44. In classical logic (our logic) this is always true. In intuitionistic logic this is not always true, and formulas for which it is true are called "stable". (Contributed by NM, 29-Dec-1992.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Ref | Expression |
---|---|
notnotr | ⊢ (¬ ¬ 𝜑 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.18 128 | . 2 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | |
2 | 1 | jarli 126 | 1 ⊢ (¬ ¬ 𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: notnotrd 133 con2d 134 con3d 152 notnotb 314 ecase3adOLD 1035 necon1ad 2957 necon4bd 2960 noetasuplem4 27463 eulercrct 29750 notornotel1 37266 mpobi123f 37333 mptbi12f 37337 oexpreposd 41514 axfrege31 42886 clsk1independent 43099 con3ALT2 43593 zfregs2VD 43904 con3ALTVD 43979 notnotrALT2 43990 suplesup 44348 |
Copyright terms: Public domain | W3C validator |