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

Theorem notnotr 128
 Description: Double negation elimination. Converse of notnot 138 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.)
Assertion
Ref Expression
notnotr (¬ ¬ 𝜑𝜑)

Proof of Theorem notnotr
StepHypRef Expression
1 pm2.18 123 . 2 ((¬ 𝜑𝜑) → 𝜑)
21jarli 127 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  130  con2d  131  con3d  149  notnotb  304  ecase3ad  1021  necon1ad  2959  necon4bd  2962  eulercrct  27419  noetalem3  32196  notornotel1  34222  mpt2bi123f  34296  mptbi12f  34300  axfrege31  38646  clsk1independent  38863  con3ALT2  39255  zfregs2VD  39592  con3ALTVD  39668  notnotrALT2  39679  suplesup  40065
 Copyright terms: Public domain W3C validator