![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > notnotrd | Structured version Visualization version GIF version |
Description: Deduction associated with notnotr 130 and notnotri 131. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 30200. 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.) |
Ref | Expression |
---|---|
notnotrd.1 | ⊢ (𝜑 → ¬ ¬ 𝜓) |
Ref | Expression |
---|---|
notnotrd | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotrd.1 | . 2 ⊢ (𝜑 → ¬ ¬ 𝜓) | |
2 | notnotr 130 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
3 | 1, 2 | syl 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 817 ecase2d 1028 efald 1555 necon1ai 2963 supgtoreq 9485 konigthlem 10583 indpi 10922 sqrmo 15222 2sqcoprm 27355 axtgupdim2 28262 ncoltgdim2 28356 ex-natded5.13 30212 bnj1204 34579 knoppndvlem10 35932 hashnexinj 41531 supxrgere 44638 supxrgelem 44642 supxrge 44643 iccdifprioo 44824 icccncfext 45198 stirlinglem5 45389 sge0repnf 45697 sge0split 45720 nnfoctbdjlem 45766 nabctnabc 46236 |
Copyright terms: Public domain | W3C validator |