Theorem notnotri 106

Description: Inference from double negation. (Contributed by NM, 27-Feb-2008.)

Hypothesis

Ref	Expression
notnotri.1	⊢ ¬ ¬ φ

Assertion

Ref	Expression
notnotri	⊢ φ

Proof of Theorem notnotri

Step	Hyp	Ref	Expression
1		notnotri.1	. 2 ⊢ ¬ ¬ φ
2		notnot2 104	. 2 ⊢ (¬ ¬ φ → φ)
3	1, 2	ax-mp 5	1 ⊢ φ

This proof depends on syntax axioms:  ¬ wn 3

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt3  171  mtp-xor  1536