notnotri - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem notnotri 100

Description: Inference from double negation.

**Hypothesis**
Ref	Expression
negai.1

**Assertion**
Ref	Expression
notnotri

**Proof of Theorem notnotri**
Step	Hyp	Ref	Expression
1		negai.1	. 2
2		notnot2 99	. 2
3	1, 2	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:

wn 2

This theorem is referenced by: heiborlem40 15676

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