Theorem notnotri 106

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

Hypothesis

Ref	Expression
notnotri.1	|- -. -. ph

Assertion

Ref	Expression
notnotri	|- ph

Proof of Theorem notnotri

Step	Hyp	Ref	Expression
1		notnotri.1	. 2 |- -. -. ph
2		notnot2 104	. 2 |- (-. -. ph -> ph)
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:  -. wn 3

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

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