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

Theorem notnotr 123
Description: Double negation elimination. Converse of notnot 134 and one implication of notnotb 302. 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.21 118 . 2 (¬ ¬ 𝜑 → (¬ 𝜑𝜑))
21pm2.18d 122 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  125  notnotrd  126  con2d  127  con3d  146  notnotb  302  ecase3ad  982  necon1ad  2798  necon4bd  2801  notornotel1  32850  mpt2bi123f  32924  mptbi12f  32928  axfrege31  36930  clsk1independent  37147  con3ALT2  37540  zfregs2VD  37881  con3ALTVD  37957  notnotrALT2  37968  suplesup  38279  eulercrct  41391
  Copyright terms: Public domain W3C validator