![]() |
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 139 and one implication of notnotb 307. 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 125 | . 2 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | |
2 | 1 | jarli 124 | 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 131 con2d 132 con3d 150 notnotb 307 ecase3ad 1063 necon1ad 3016 necon4bd 3019 eulercrct 27615 noetalem3 32399 notornotel1 34437 mpt2bi123f 34510 mptbi12f 34514 oexpreposd 38067 axfrege31 38966 clsk1independent 39183 con3ALT2 39573 zfregs2VD 39894 con3ALTVD 39969 notnotrALT2 39980 suplesup 40350 |
Copyright terms: Public domain | W3C validator |