Metamath Proof Explorer


Theorem notnotrALT2

Description: Converse of double negation. Theorem *2.14 of WhiteheadRussell p. 102. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion notnotrALT2 ¬ ¬ φ φ

Proof

Step Hyp Ref Expression
1 notnotr ¬ ¬ φ φ