![]() |
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 315. 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 315 necon1ad 2956 necon4bd 2959 noetasuplem4 27771 eulercrct 30251 expgt0b 32806 notornotel1 38080 mpobi123f 38147 mptbi12f 38151 oexpreposd 42335 axfrege31 43824 clsk1independent 44037 con3ALT2 44528 zfregs2VD 44839 con3ALTVD 44914 notnotrALT2 44925 suplesup 45323 |
Copyright terms: Public domain | W3C validator |