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

Theorem notnotr 130
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.)
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  133  con2d  134  con3d  152  notnotb  315  ecase3adOLD  1036  necon1ad  2961  necon4bd  2964  noetasuplem4  27100  eulercrct  29228  notornotel1  36583  mpobi123f  36650  mptbi12f  36654  oexpreposd  40836  axfrege31  42179  clsk1independent  42392  con3ALT2  42886  zfregs2VD  43197  con3ALTVD  43272  notnotrALT2  43283  suplesup  43647
  Copyright terms: Public domain W3C validator