MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnotr Structured version   Visualization version   GIF version

Theorem notnotr 132
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.)
Assertion
Ref Expression
notnotr (¬ ¬ 𝜑𝜑)

Proof of Theorem notnotr
StepHypRef Expression
1 pm2.18 128 . 2 ((¬ 𝜑𝜑) → 𝜑)
21jarli 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