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

Theorem notnotrd 130
 Description: Deduction associated with notnotr 128 and notnotri 129. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 27602. This is Definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (our logic), but not in intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)
Hypothesis
Ref Expression
notnotrd.1 (𝜑 → ¬ ¬ 𝜓)
Assertion
Ref Expression
notnotrd (𝜑𝜓)

Proof of Theorem notnotrd
StepHypRef Expression
1 notnotrd.1 . 2 (𝜑 → ¬ ¬ 𝜓)
2 notnotr 128 . 2 (¬ ¬ 𝜓𝜓)
31, 2syl 17 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:  condan  819  efald  1652  necon1ai  2970  supgtoreq  8536  konigthlem  9596  indpi  9935  sqrmo  14200  axtgupdim2  25591  ncoltgdim2  25681  ex-natded5.13  27614  2sqcoprm  29987  bnj1204  31418  knoppndvlem10  32849  supxrgere  40062  supxrgelem  40066  supxrge  40067  iccdifprioo  40258  icccncfext  40615  stirlinglem5  40809  sge0repnf  41117  sge0split  41140  nnfoctbdjlem  41186  nabctnabc  41615
 Copyright terms: Public domain W3C validator