Theorem notnotb

Description: Double negation. Theorem *4.13 of WhiteheadRussell p. 117. (Contributed by NM, 3-Jan-1993)

	Ref	Expression
Assertion	notnotb	⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		notnot	⊢ ( 𝜑 → ¬ ¬ 𝜑 )
2		notnotr	⊢ ( ¬ ¬ 𝜑 → 𝜑 )
3	1 2	impbii	⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 )