![]() |
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 136 and one implication of notnotb 304. 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.21 120 | . 2 ⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → 𝜑)) | |
2 | 1 | pm2.18d 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: notnotriOLD 127 notnotrd 128 con2d 129 con3d 148 notnotb 304 ecase3ad 1005 necon1ad 2840 necon4bd 2843 eulercrct 27220 noetalem3 31990 notornotel1 34027 mpt2bi123f 34101 mptbi12f 34105 axfrege31 38444 clsk1independent 38661 con3ALT2 39053 zfregs2VD 39390 con3ALTVD 39466 notnotrALT2 39477 suplesup 39868 |
Copyright terms: Public domain | W3C validator |