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 139 and one implication of notnotb 307. 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 125 . 2 ((¬ 𝜑𝜑) → 𝜑)
21jarli 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:  notnotrd  131  con2d  132  con3d  150  notnotb  307  ecase3ad  1063  necon1ad  3016  necon4bd  3019  eulercrct  27615  noetalem3  32399  notornotel1  34437  mpt2bi123f  34510  mptbi12f  34514  oexpreposd  38067  axfrege31  38966  clsk1independent  39183  con3ALT2  39573  zfregs2VD  39894  con3ALTVD  39969  notnotrALT2  39980  suplesup  40350
 Copyright terms: Public domain W3C validator