negai - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem negai 85

Description: Inference from double negation.

**Hypothesis**
Ref	Expression
negai.1

**Assertion**
Ref	Expression
negai

**Proof of Theorem negai**
Step	Hyp	Ref	Expression
1		negai.1	. 2
2		nega 84	. 2
3	1, 2	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:

wn 2

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