![]() |
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 1034 necon1ad 2954 necon4bd 2957 noetasuplem4 27689 eulercrct 30072 notornotel1 37601 mpobi123f 37668 mptbi12f 37672 oexpreposd 41912 axfrege31 43294 clsk1independent 43507 con3ALT2 44000 zfregs2VD 44311 con3ALTVD 44386 notnotrALT2 44397 suplesup 44750 |
Copyright terms: Public domain | W3C validator |