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 
|- ( ph <-> -. -. ph )

Proof

Step Hyp Ref Expression
1 notnot 
 |-  ( ph -> -. -. ph )
2 notnotr 
 |-  ( -. -. ph -> ph )
3 1 2 impbii 
 |-  ( ph <-> -. -. ph )