notnotrd - Metamath Proof Explorer

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

Theorem notnotrd 113

Description: Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule -.-. -C, |--.-. => |-; see natded 25124. This is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)

**Hypothesis**
Ref	Expression
notnotrd.1

**Assertion**
Ref	Expression
notnotrd

**Proof of Theorem notnotrd**
Step	Hyp	Ref	Expression
1		notnotrd.1	. 2
2		notnot2 112	. 2
3	1, 2	syl 16	1

Colors of variables: wff setvar class

Syntax hints: -.wn 3 ->wi 4

This theorem is referenced by: condan 794 efald 1417 necon1ai 2688 supgtoreq 7949 konigthlem 8964 indpi 9306 sqrmo 13085 ncoltgdim2 23952 ex-natded5.13 25136 2sqcoprm 27635 iccdifprioo 31556 icccncfext 31690 stirlinglem5 31860 bnj1204 34068

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

W3C validator