Metamath Proof Explorer


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 φ¬¬φ