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 144 and one implication of notnotb 318. 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 135 con2d 136 con3d 155 notnotb 318 ecase3adOLD 1037 necon1ad 2960 necon4bd 2963 eulercrct 28357 noetasuplem4 33710 notornotel1 36027 mpobi123f 36094 mptbi12f 36098 oexpreposd 40077 axfrege31 41166 clsk1independent 41381 con3ALT2 41871 zfregs2VD 42182 con3ALTVD 42257 notnotrALT2 42268 suplesup 42599 |
Copyright terms: Public domain | W3C validator |