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

Proof

Step Hyp Ref Expression
1 notnotr
 |-  ( -. -. ph -> ph )